test/Tools/isac/Knowledge/algein.sml
branchdecompose-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