changeset 90 | 5c7a69cef18b |
parent 0 | 7949f97df77a |
child 108 | 82c4117aff7f |
--- a/Trancl.ML Fri Jun 24 15:11:39 1994 +0200 +++ b/Trancl.ML Wed Jun 29 12:04:04 1994 +0200 @@ -151,7 +151,7 @@ "[| <a::'a,b> : r^*; (a = b) ==> P; \ \ !!y.[| <a,y> : r^*; <y,b> : r |] ==> P \ \ |] ==> P"; -by (subgoal_tac "a::'a = b | (? y. <a,y> : r^* & <y,b> : r)" 1); +by (subgoal_tac "(a::'a) = b | (? y. <a,y> : r^* & <y,b> : r)" 1); by (rtac (major RS rtrancl_induct) 2); by (fast_tac (set_cs addIs prems) 2); by (fast_tac (set_cs addIs prems) 2);