1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Fri Feb 23 07:29:36 2018 +0100
     1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Sat Feb 24 11:14:56 2018 +0100
     1.3 @@ -23,6 +23,7 @@
     1.4  "----------- repair NO asms from rls RatEq_eliminate ----";
     1.5  "----------- fun assoc_thm' -----------------------------";
     1.6  "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
     1.7 +"----------- fun mk_thm ------------------------------------------------------------------------";
     1.8  "--------------------------------------------------------";
     1.9  "--------------------------------------------------------";
    1.10  "--------------------------------------------------------";
    1.11 @@ -587,3 +588,33 @@
    1.12  val match = Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty);
    1.13  if (Envir.subst_term match r |> term2str) = "x * (y + z) = x * y + x * z" then ()
    1.14    else error "Pattern.match CHANGED";
    1.15 +
    1.16 +"----------- fun mk_thm ------------------------------------------------------------------------";
    1.17 +"----------- fun mk_thm ------------------------------------------------------------------------";
    1.18 +"----------- fun mk_thm ------------------------------------------------------------------------";
    1.19 +(*
    1.20 +  val str = "?r ^^^ 2 = ?r * ?r";
    1.21 +  val thm = realpow_twoI;
    1.22 +
    1.23 +  val t1 = (#prop o rep_thm) (num_str thm);
    1.24 +  val t2 = Trueprop $ ((Thm.term_of o the o (parse thy)) str);
    1.25 +  t1 = t2;
    1.26 +val it = true : bool      ... !!!
    1.27 +  val th1 = (num_str thm);
    1.28 +  val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
    1.29 +  th1 = th2;
    1.30 +ML> val it = false : bool ... HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
    1.31 +
    1.32 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    1.33 +  val str = "k ~= 0 ==> m * k / (n * k) = m / n";
    1.34 +  val thm = real_mult_div_cancel2;
    1.35 +
    1.36 +  val t1 = (#prop o rep_thm) (num_str thm);
    1.37 +  val t2 = ((Thm.term_of o the o (parse thy)) str);
    1.38 +  t1 = t2;
    1.39 +val it = false : bool     ... Var .. Free
    1.40 +  val th1 = (num_str thm);
    1.41 +  val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
    1.42 +  th1 = th2;
    1.43 +ML> val it = false : bool ... PLUS HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
    1.44 +*)