;; emacs lisp file for typechecking/proving this context
;; generated by prove.pl - do not edit !

(setq files '(
 "abs"
 "adder_add"
 "adder_adder"
 "adder_au"
 "adder_basic"
 "adder_cc"
 "adder_compound"
 "adder_condsum"
 "adder_csa"
 "adder_faha"
 "adder_inc"
 "adder_lem"
 "adder_sub"
 "adder_top"
 "decoder"
 "enc"
 "lzero"
 "misc"
 "mult_lin"
 "multiplier"
 "pp"
 "shifter"
 "zero"
 "mult_karatsuba"
 "mux_tree"
 "basics_import"
 "neg"
))

(setq current-prefix-arg t)
(mapcar (lambda (f)
;  (pvs-message (concat "\n--> Typechecking " f))
  (typecheck f)
  ;  (prove-pvs-file f)
  )
  files)
  (save-context)
  (message "Leaving...")
  (exit-pvs)
  (message "Killing...")
  (kill-emacs)