diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/ex/Acc.ML
--- a/src/HOL/ex/Acc.ML	Tue Jan 30 15:19:20 1996 +0100
+++ b/src/HOL/ex/Acc.ML	Tue Jan 30 15:24:36 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/ex/Acc
+(*  Title:      HOL/ex/Acc
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
 Inductive definition of acc(r)
@@ -15,7 +15,7 @@
 val prems = goal Acc.thy
     "[| !!b. (b,a):r ==> b: acc(r) |] ==> a: acc(r)";
 by (fast_tac (set_cs addIs (prems @ 
-			    map (rewrite_rule [pred_def]) acc.intrs)) 1);
+                            map (rewrite_rule [pred_def]) acc.intrs)) 1);
 qed "accI";
 
 goal Acc.thy "!!a b r. [| b: acc(r);  (a,b): r |] ==> a: acc(r)";
@@ -25,8 +25,8 @@
 qed "acc_downward";
 
 val [major,indhyp] = goal Acc.thy
-    "[| a : acc(r);						\
-\       !!x. [| x: acc(r);  ALL y. (y,x):r --> P(y) |] ==> P(x)	\
+    "[| a : acc(r);                                             \
+\       !!x. [| x: acc(r);  ALL y. (y,x):r --> P(y) |] ==> P(x) \
 \    |] ==> P(a)";
 by (rtac (major RS acc.induct) 1);
 by (rtac indhyp 1);
@@ -55,7 +55,7 @@
 by (rtac subsetI 1);
 by (res_inst_tac [("p", "x")] PairE 1);
 by (fast_tac (set_cs addSIs [SigmaI,
-			     major RS acc_wfD_lemma RS spec RS mp]) 1);
+                             major RS acc_wfD_lemma RS spec RS mp]) 1);
 qed "acc_wfD";
 
 goal Acc.thy "wf(r)  =  (r <= Sigma (acc r) (%u. acc(r)))";