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

(setq files '(
 "add_correct"
 "add_ctl"
 "add_def"
 "add_synth"
 "add_tomcirc"
 "fpm_correct"
 "fpm_ctl"
 "fpm_def"
 "fpm_syth"
 "fpm_tomcirc"
 "fpu_import_add"
 "fpu_import_md"
 "md_correct"
 "md_ctl"
 "md_def"
 "md_synth"
 "md_tomcirc"
 "signals"
 "tag"
 "tom_ciruit"
 "unchanged"
 "fpu_import_misc"
))

(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)