changeset 69266 | 7cc2d66a92a6 |
parent 69064 | 5840724b1d71 |
child 69313 | b021008c5397 |
--- a/src/HOL/Decision_Procs/MIR.thy Thu Nov 08 14:58:04 2018 +0100 +++ b/src/HOL/Decision_Procs/MIR.thy Thu Nov 08 15:49:56 2018 +0100 @@ -5682,7 +5682,7 @@ val qe = if Config.get ctxt quick_and_dirty then @{code mircfrqe} else @{code mirlfrqe}; val t' = term_of_fm vs (qe (fm_of_term vs t)); in Thm.cterm_of ctxt (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) end -end; +end \<close> lemmas iff_real_of_int = of_int_eq_iff [where 'a = real, symmetric]