# HG changeset patch
# User paulson
# Date 830518226 -7200
# Node ID fbbd65c89c23855c00e09a43f170007f142210b9
# Parent  e0ff33a33fa53660334c70ed5ebd005708898a0e
Fixed indenting

diff -r e0ff33a33fa5 -r fbbd65c89c23 src/HOL/ex/Comb.ML
--- 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)]