1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Mon Apr 20 10:27:19 2015 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Mon Apr 20 10:33:55 2015 +0200
     1.3 @@ -21,6 +21,7 @@
     1.4  "----------- fun app_rev, Rrls, -------------------------";
     1.5  "----------- 2011 thms with axclasses -------------------";
     1.6  "----------- repair NO asms from rls RatEq_eliminate ----";
     1.7 +"----------- fun assoc_thm' -----------------------------";
     1.8  "--------------------------------------------------------";
     1.9  "--------------------------------------------------------";
    1.10  "--------------------------------------------------------";
    1.11 @@ -541,3 +542,24 @@
    1.12  trace_rewrite := false;
    1.13  (* WN120317.TODO dropped rateq: the above error is the same in 2002 *)
    1.14  
    1.15 +"----------- fun assoc_thm' -----------------------------";
    1.16 +"----------- fun assoc_thm' -----------------------------";
    1.17 +"----------- fun assoc_thm' -----------------------------";
    1.18 +val thy = @{theory ProgLang}
    1.19 +
    1.20 +val tth = assoc_thm' thy ("sym_#mult_2_3","6 = 2 * 3");
    1.21 +if string_of_thm' thy tth = "6 = 2 * 3" then ()
    1.22 +else error "assoc_thm' (sym_#mult_2_3, 6 = 2 * 3) changed";
    1.23 +
    1.24 +val tth = assoc_thm' thy ("add_0_left","");
    1.25 +if string_of_thm' thy tth = "0 + ?a = ?a" then ()
    1.26 +else error "assoc_thm' (add_0_left,\"\") changed";
    1.27 +
    1.28 +val tth = assoc_thm' thy ("sym_add_0_left","");
    1.29 +if string_of_thm' thy tth = "?t = 0 + ?t" then ()
    1.30 +else error "assoc_thm' (sym_add_0_left,\"\") changed";
    1.31 +
    1.32 +val tth = assoc_thm' thy ("add_commute","");
    1.33 +if string_of_thm' thy tth = "?a + ?b = ?b + ?a" then ()
    1.34 +else error "assoc_thm' (add_commute,\"\") changed"
    1.35 +