# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1664360629 -3600
# Node ID cf8f85e2a8071b8ac3b5dbe4d17aadfd56a66d99
# Parent  cf7db6353322cfc5e10d33c05bd21fc1fea69991
fixed some theory presentation issues (?)

diff -r cf7db6353322 -r cf8f85e2a807 src/ZF/AC/HH.thy
--- a/src/ZF/AC/HH.thy	Wed Sep 28 11:00:13 2022 +0200
+++ b/src/ZF/AC/HH.thy	Wed Sep 28 11:23:49 2022 +0100
@@ -126,7 +126,7 @@
 apply (erule_tac [2] ltI [OF _ Ord_Least], assumption)
 done
 
-subsection\<open>Lemmas used in the proofs of AC1 \<Longrightarrow> WO2 and AC17 \<Longrightarrow> AC1\<close>
+subsection\<open>Lemmas used in the proofs of @{term "AC1 \<Longrightarrow> WO2"} and @{term "AC17 \<Longrightarrow> AC1"}\<close>
 
 lemma lam_Least_HH_inj_Pow: 
         "(\<lambda>a \<in> (\<mu> i. HH(f,x,i)={x}). HH(f,x,a))   
@@ -213,7 +213,7 @@
               lam_sing_bij [THEN bij_converse_bij]]
 
 
-subsection\<open>The proof of AC1 \<Longrightarrow> WO2\<close>
+subsection\<open>The proof of @{term "AC1 \<Longrightarrow> WO2"}\<close>
 
 (*Establishing the existence of a bijection, namely
 converse
@@ -236,10 +236,9 @@
 
 lemma AC1_WO2: "AC1 \<Longrightarrow> WO2"
   unfolding AC1_def WO2_def eqpoll_def
-apply (intro allI) 
-apply (drule_tac x = "Pow(A) - {0}" in spec) 
-apply (blast dest: bijection)
-done
+  apply (intro allI) 
+  apply (drule_tac x = "Pow(A) - {0}" in spec) 
+  apply (blast dest: bijection)
+  done
 
 end
-
diff -r cf7db6353322 -r cf8f85e2a807 src/ZF/Constructible/AC_in_L.thy
--- a/src/ZF/Constructible/AC_in_L.thy	Wed Sep 28 11:00:13 2022 +0200
+++ b/src/ZF/Constructible/AC_in_L.thy	Wed Sep 28 11:23:49 2022 +0100
@@ -453,7 +453,7 @@
 
 
 text\<open>Every constructible set is well-ordered! Therefore the Wellordering Theorem and
-      the Axiom of Choice hold in \<^term>\<open>L\<close>\<And>\<close>
+      the Axiom of Choice hold in \<^term>\<open>L\<close>!\<close>
 theorem L_implies_AC: assumes x: "L(x)" shows "\<exists>r. well_ord(x,r)"
   using Transset_Lset x
 apply (simp add: Transset_def L_def)
diff -r cf7db6353322 -r cf8f85e2a807 src/ZF/Constructible/DPow_absolute.thy
--- a/src/ZF/Constructible/DPow_absolute.thy	Wed Sep 28 11:00:13 2022 +0200
+++ b/src/ZF/Constructible/DPow_absolute.thy	Wed Sep 28 11:23:49 2022 +0100
@@ -13,7 +13,7 @@
 subsubsection\<open>The Operator \<^term>\<open>is_formula_rec\<close>\<close>
 
 text\<open>The three arguments of \<^term>\<open>p\<close> are always 2, 1, 0.  It is buried
-   within 11 quantifiers\<And>\<close>
+   within 11 quantifiers!\<close>
 
 (* is_formula_rec :: "[i\<Rightarrow>o, [i,i,i]\<Rightarrow>o, i, i] \<Rightarrow> o"
    "is_formula_rec(M,MH,p,z)  \<equiv>
@@ -595,15 +595,10 @@
 subsubsection\<open>Actually Instantiating \<open>M_Lset\<close>\<close>
 
 lemma M_Lset_axioms_L: "M_Lset_axioms(L)"
-  apply (rule M_Lset_axioms.intro)
-       apply (assumption | rule strong_rep transrec_rep)+
-  done
+  by (blast intro: M_Lset_axioms.intro strong_rep transrec_rep)
 
 theorem M_Lset_L: "M_Lset(L)"
-  apply (rule M_Lset.intro) 
-   apply (rule M_DPow_L)
-  apply (rule M_Lset_axioms_L) 
-  done
+  by (blast intro: M_Lset.intro M_DPow_L M_Lset_axioms_L)
 
 text\<open>Finally: the point of the whole theory!\<close>
 lemmas Lset_closed = M_Lset.Lset_closed [OF M_Lset_L]
@@ -619,9 +614,12 @@
 
 theorem V_equals_L_in_L:
   "L(x) \<longleftrightarrow> constructible(L,x)"
-apply (simp add: constructible_def Lset_abs Lset_closed)
-apply (simp add: L_def)
-apply (blast intro: Ord_in_L) 
-done
+proof -
+  have "L(x) \<longleftrightarrow> (\<exists>i[L]. Ord(i) \<and> x \<in> Lset(i))"
+    by (auto simp add: L_def intro: Ord_in_L)
+  moreover have "\<dots> \<longleftrightarrow> constructible(L,x)"
+    by (simp add: constructible_def Lset_abs Lset_closed)
+  ultimately show ?thesis by blast
+qed
 
 end