src/HOL/UNITY/Simple/Reach.thy
changeset 15076 4b3d280ef06a
parent 14150 9a23e4eb5eb3
child 15097 b807858b97bd
--- a/src/HOL/UNITY/Simple/Reach.thy	Thu Jul 22 19:33:12 2004 +0200
+++ b/src/HOL/UNITY/Simple/Reach.thy	Mon Jul 26 15:48:50 2004 +0200
@@ -75,7 +75,7 @@
 apply (unfold fixedpoint_def)
 apply (rule equalityI)
 apply (auto intro!: ext)
- prefer 2 apply (blast intro: rtrancl_trans)
+(* CBtrancl: prefer 2 apply (blast intro: rtrancl_trans) *)
 apply (erule rtrancl_induct, auto)
 done