src/ZF/Constructible/AC_in_L.thy

 (*  Title:      ZF/Constructible/AC_in_L.thy
-    ID: $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
 header {* The Axiom of Choice Holds in L! *}
 

 definition
   env_form_r :: "[i,i,i]=>i" where
     --{*wellordering on (environment, formula) pairs*}
    "env_form_r(f,r,A) ==
       rmult(list(A), rlist(A, r),
-	    formula, measure(formula, enum(f)))"
+            formula, measure(formula, enum(f)))"
 
 definition
   env_form_map :: "[i,i,i,i]=>i" where
     --{*map from (environment, formula) pairs to ordinals*}
    "env_form_map(f,r,A,z)

   rlimit :: "[i,i=>i]=>i" where
   --{*Expresses the wellordering at limit ordinals.  The conditional
       lets us remove the premise @{term "Limit(i)"} from some theorems.*}
     "rlimit(i,r) ==
        if Limit(i) then 
-	 {z: Lset(i) * Lset(i).
-	  \<exists>x' x. z = <x',x> &
-		 (lrank(x') < lrank(x) |
-		  (lrank(x') = lrank(x) & <x',x> \<in> r(succ(lrank(x)))))}
+         {z: Lset(i) * Lset(i).
+          \<exists>x' x. z = <x',x> &
+                 (lrank(x') < lrank(x) |
+                  (lrank(x') = lrank(x) & <x',x> \<in> r(succ(lrank(x)))))}
        else 0"
 
 definition
   Lset_new :: "i=>i" where
   --{*This constant denotes the set of elements introduced at level