1.1 --- a/src/Tools/isac/Build_Isac.thy	Mon Dec 31 14:15:19 2018 +0100
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Mon Dec 31 14:49:16 2018 +0100
     1.3 @@ -74,36 +74,6 @@
     1.4  ML \<open>
     1.5  \<close> ML \<open>
     1.6  \<close>
     1.7 -
     1.8 -(*==============================================================================================
     1.9 -  The test below from calculate.sml raises an exception with the cleaned Rewrite.
    1.10 -  The differences to the working 'fun rewrite' are that significant,
    1.11 -  that we want to rely on 'hg revert'.
    1.12 -  For that purpose we save this changeset with a broken 'fun rewrite' and tests not running.
    1.13 -*)
    1.14 -ML \<open>
    1.15 -\<close> ML \<open>
    1.16 -(*--------------(2): does divide work in Test_simplify ?: ------*)
    1.17 - val thy = @{theory Test};
    1.18 - val t = (Thm.term_of o the o (TermC.parse thy)) "6 / 2";
    1.19 - val rls = Test_simplify;
    1.20 -\<close> ML \<open>
    1.21 - val (t,_) = the (Rewrite.rewrite_set_ thy false rls t);
    1.22 -(*val t = Free ("3","Real.real") : term*)
    1.23 -\<close> ML \<open>
    1.24 -
    1.25 -(*--------------(3): is_const works ?: -------------------------------------*)
    1.26 - val t = (Thm.term_of o the o (TermC.parse @{theory})) "2 is_const";
    1.27 -\<close> ML \<open>
    1.28 - Rewrite.rewrite_set_ @{theory Test} false tval_rls t;
    1.29 -
    1.30 -(* exception TERM raised (line 270 of "~~/src/HOL/Tools/hologic.ML"):
    1.31 -  dest_eq
    1.32 -  0 \<le> ?a \<Longrightarrow> (0 \<le> sqrt ?a) = True*)
    1.33 -\<close> ML \<open>
    1.34 -\<close>
    1.35 -(*==============================================================================================*)
    1.36 -
    1.37  ML \<open>Calc.adhoc_thm; (*from "ProgLang/calculate.sml" *)\<close>
    1.38  ML \<open>Rewrite.rewrite_; (*from "ProgLang/rewrite.sml" *)\<close>
    1.39  ML \<open>LTool.is_reall_dsc; (*from "ProgLang/scrtools.sml" *)\<close>