src/ZF/Constructible/Wellorderings.thy
changeset 32960 69916a850301
parent 21404 eb85850d3eb7
child 46823 57bf0cecb366
--- a/src/ZF/Constructible/Wellorderings.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/ZF/Constructible/Wellorderings.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Constructible/Wellorderings.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
@@ -23,30 +22,30 @@
 definition
   transitive_rel :: "[i=>o,i,i]=>o" where
     "transitive_rel(M,A,r) == 
-	\<forall>x[M]. x\<in>A --> (\<forall>y[M]. y\<in>A --> (\<forall>z[M]. z\<in>A --> 
+        \<forall>x[M]. x\<in>A --> (\<forall>y[M]. y\<in>A --> (\<forall>z[M]. z\<in>A --> 
                           <x,y>\<in>r --> <y,z>\<in>r --> <x,z>\<in>r))"
 
 definition
   linear_rel :: "[i=>o,i,i]=>o" where
     "linear_rel(M,A,r) == 
-	\<forall>x[M]. x\<in>A --> (\<forall>y[M]. y\<in>A --> <x,y>\<in>r | x=y | <y,x>\<in>r)"
+        \<forall>x[M]. x\<in>A --> (\<forall>y[M]. y\<in>A --> <x,y>\<in>r | x=y | <y,x>\<in>r)"
 
 definition
   wellfounded :: "[i=>o,i]=>o" where
     --{*EVERY non-empty set has an @{text r}-minimal element*}
     "wellfounded(M,r) == 
-	\<forall>x[M]. x\<noteq>0 --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))"
+        \<forall>x[M]. x\<noteq>0 --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))"
 definition
   wellfounded_on :: "[i=>o,i,i]=>o" where
     --{*every non-empty SUBSET OF @{text A} has an @{text r}-minimal element*}
     "wellfounded_on(M,A,r) == 
-	\<forall>x[M]. x\<noteq>0 --> x\<subseteq>A --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))"
+        \<forall>x[M]. x\<noteq>0 --> x\<subseteq>A --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))"
 
 definition
   wellordered :: "[i=>o,i,i]=>o" where
     --{*linear and wellfounded on @{text A}*}
     "wellordered(M,A,r) == 
-	transitive_rel(M,A,r) & linear_rel(M,A,r) & wellfounded_on(M,A,r)"
+        transitive_rel(M,A,r) & linear_rel(M,A,r) & wellfounded_on(M,A,r)"
 
 
 subsubsection {*Trivial absoluteness proofs*}
@@ -221,7 +220,7 @@
     "[| wellordered(M,A,r);  B<=A |] ==> wellordered(M,B,r)"
 apply (unfold wellordered_def)
 apply (blast intro: linear_rel_subset transitive_rel_subset 
-		    wellfounded_on_subset)
+                    wellfounded_on_subset)
 done
 
 lemma (in M_basic) wellfounded_on_asym: