proper ML expressions, without trailing semicolons;
authorwenzelm
Thu Nov 08 15:49:56 2018 +0100 (6 months ago)
changeset 692667cc2d66a92a6
parent 69265 bd215c56cd96
child 69267 517655a528fe
proper ML expressions, without trailing semicolons;
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
     1.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Thu Nov 08 14:58:04 2018 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Thu Nov 08 15:49:56 2018 +0100
     1.3 @@ -2524,7 +2524,7 @@
     1.4        val ps = map_index swap bs;
     1.5        val t' = term_of_fm ps vs (@{code pa} (fm_of_term ps vs t));
     1.6      in Thm.cterm_of ctxt (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) end
     1.7 -end;
     1.8 +end
     1.9  \<close>
    1.10  
    1.11  ML_file "cooper_tac.ML"
     2.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Thu Nov 08 14:58:04 2018 +0100
     2.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Thu Nov 08 15:49:56 2018 +0100
     2.3 @@ -2543,7 +2543,7 @@
     2.4      val vs = Term.add_frees t [];
     2.5      val t' = (term_of_fm vs o @{code linrqe} o fm_of_term vs) t;
     2.6    in (Thm.cterm_of ctxt o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
     2.7 -end;
     2.8 +end
     2.9  \<close>
    2.10  
    2.11  ML_file "ferrack_tac.ML"
     3.1 --- a/src/HOL/Decision_Procs/MIR.thy	Thu Nov 08 14:58:04 2018 +0100
     3.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Thu Nov 08 15:49:56 2018 +0100
     3.3 @@ -5682,7 +5682,7 @@
     3.4      val qe = if Config.get ctxt quick_and_dirty then @{code mircfrqe} else @{code mirlfrqe};
     3.5      val t' = term_of_fm vs (qe (fm_of_term vs t));
     3.6    in Thm.cterm_of ctxt (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) end
     3.7 -end;
     3.8 +end
     3.9  \<close>
    3.10  
    3.11  lemmas iff_real_of_int = of_int_eq_iff [where 'a = real, symmetric]