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

(setq files '(
 "mul_div_import"
 "div_initial"
 "div_rep"
 "exp_md"
 "ieee_md"
 "lookup"
 "md_stg1"
 "md_stg2"
 "mul_div_comb"
 "newton1"
 "newton_fin"
 "select_fd"
 "ieee_md"
 "md_unpack"
 "md_comb"
))

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