src/HOL/ex/Comb.ML
changeset 1691 fbbd65c89c23
parent 1689 c38d953caedb
child 1730 1c7f793fc374
--- a/src/HOL/ex/Comb.ML	Fri Apr 26 12:33:30 1996 +0200
+++ b/src/HOL/ex/Comb.ML	Fri Apr 26 13:30:26 1996 +0200
@@ -26,8 +26,8 @@
 
 (*Strip lemma.  The induction hyp is all but the last diamond of the strip.*)
 goalw Comb.thy [diamond_def]
-    "!!x y r. [| diamond(r);  (x,y):r^* |] ==> \
-\    ALL y'. (x,y'):r --> (EX z. (y',z): r^* & (y,z): r)";
+    "!!r. [| diamond(r);  (x,y):r^* |] ==> \ 
+\         ALL y'. (x,y'):r --> (EX z. (y',z): r^* & (y,z): r)";
 by (etac rtrancl_induct 1);
 by (fast_tac (HOL_cs addIs [rtrancl_refl]) 1);
 by (slow_best_tac (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)]