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