1.1 --- a/test/Tools/isac/Knowledge/algein.sml Tue Apr 14 15:56:15 2020 +0200
1.2 +++ b/test/Tools/isac/Knowledge/algein.sml Wed Apr 15 10:07:43 2020 +0200
1.3 @@ -103,7 +103,7 @@
1.4 val thy = @{theory "Isac_Knowledge"};
1.5 val rew_ord = dummy_ord;
1.6 val erls = Rule_Set.Empty;
1.7 -val thm = assoc_thm'' thy "sym_mult_zero_right";
1.8 +val thm = ThmC.thm_from_thy thy "sym_mult_zero_right";
1.9 val t = str2term "0 = (0::real)";
1.10 val SOME (t',_) = rewrite_ thy rew_ord erls false thm t;
1.11 UnparseC.term t' = "0 = ?a1 * 0"; (* = true*)
1.12 @@ -118,7 +118,7 @@
1.13 val t'' = subst_atomic subst t';
1.14 UnparseC.term t'' = "0 = 3 * 0"; (* = true*)
1.15
1.16 -val thm = assoc_thm'' thy "sym";
1.17 +val thm = ThmC.thm_from_thy thy "sym";
1.18 (*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!
1.19 val SOME (t''',_) = rewrite_ thy rew_ord erls false thm t'';
1.20 *)