1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Thu Mar 15 15:48:52 2018 +0100
     1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Fri Mar 23 10:14:39 2018 +0100
     1.3 @@ -24,6 +24,7 @@
     1.4  "----------- fun assoc_thm' -----------------------------";
     1.5  "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
     1.6  "----------- fun mk_thm ------------------------------------------------------------------------";
     1.7 +"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
     1.8  "--------------------------------------------------------";
     1.9  "--------------------------------------------------------";
    1.10  "--------------------------------------------------------";
    1.11 @@ -654,3 +655,17 @@
    1.12  
    1.13  val t1' = (#prop o Thm.rep_thm) (num_str thm_made);
    1.14  if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";
    1.15 +
    1.16 +"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
    1.17 +"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
    1.18 +"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
    1.19 +(* norm_equation is defined in Test.thy, other rls see Knowledg/**)
    1.20 +val thy = @{theory};
    1.21 +val rls = norm_equation;
    1.22 +val term = str2term "x + 1 = 2";
    1.23 +
    1.24 +val SOME (t, asm) = rewrite_set_ thy false rls term;
    1.25 +if term2str t = "x + 1 + -1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED";
    1.26 +
    1.27 +"~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (thy, false, rls, term);
    1.28 +"~~~~~ fun rewrite__set_, args:"; val (thy, i, put_asm, bdv, rls, ct) = (thy, 1, bool, [], rls, term);