branch | decompose-isar |
changeset 41977 | a3ce4017f41d |
parent 41943 | f33f6959948b |
child 42166 | 911c49949ba9 |
1.1 --- a/test/Tools/isac/Knowledge/algein.sml Thu May 05 14:21:54 2011 +0200 1.2 +++ b/test/Tools/isac/Knowledge/algein.sml Fri May 06 11:18:07 2011 +0200 1.3 @@ -150,7 +150,7 @@ 1.4 (********"0 = 3 * 0"*) 1.5 1.6 val thm = assoc_thm' thy ("sym",""); 1.7 -(*----- GOON Widerspruch 3 = 777: sym contains "==>" instead of "=" !!! 1.8 +(*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!! 1.9 val SOME (t''',_) = rewrite_ thy rew_ord erls false thm t''; 1.10 *) 1.11