# HG changeset patch
# User paulson
# Date 1332434482 0
# Node ID 2e3dcec916539aa9b4eb3667ee7b008d10eac3c3
# Parent  d04b38d4035b305a978809b4ded55765175a177d
New Message

diff -r d04b38d4035b -r 2e3dcec91653 src/ZF/Constructible/AC_in_L.thy
--- a/src/ZF/Constructible/AC_in_L.thy	Thu Mar 22 10:10:02 2012 +0100
+++ b/src/ZF/Constructible/AC_in_L.thy	Thu Mar 22 16:41:22 2012 +0000
@@ -4,7 +4,7 @@
 
 header {* The Axiom of Choice Holds in L! *}
 
-theory AC_in_L imports Formula begin
+theory AC_in_L imports Formula Separation begin
 
 subsection{*Extending a Wellordering over a List -- Lexicographic Power*}
 
@@ -452,6 +452,18 @@
 apply (blast dest!: well_ord_L_r intro: well_ord_subset)
 done
 
+interpretation L?: M_basic L by (rule M_basic_L)
+
+theorem "\<forall>x[L]. \<exists>r. wellordered(L,x,r)"
+proof 
+  fix x
+  assume "L(x)"
+  then obtain r where "well_ord(x,r)" 
+    by (blast dest: L_implies_AC) 
+  thus "\<exists>r. wellordered(L,x,r)" 
+    by (blast intro: well_ord_imp_relativized)
+qed
+
 text{*In order to prove @{term" \<exists>r[L]. wellordered(L, A, r)"}, it's necessary to know 
 that @{term r} is actually constructible. Of course, it follows from the assumption ``@{term V} equals @{term L''}, 
 but this reasoning doesn't appear to work in Isabelle.*}