# HG changeset patch
# User haftmann
# Date 1216964153 -7200
# Node ID 85ea2be46c714d5fcdea39fabf28fb6bd898b579
# Parent  646ea25ff59d6bae45ece05918d8097d401c0aa4
dropped locale (open)

diff -r 646ea25ff59d -r 85ea2be46c71 src/ZF/AC/AC15_WO6.thy
--- a/src/ZF/AC/AC15_WO6.thy	Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/AC15_WO6.thy	Fri Jul 25 07:35:53 2008 +0200
@@ -20,7 +20,9 @@
 Rubin & Rubin do.
 *)
 
-theory AC15_WO6 imports HH Cardinal_aux begin
+theory AC15_WO6
+imports HH Cardinal_aux
+begin
 
 
 (* ********************************************************************** *)
diff -r 646ea25ff59d -r 85ea2be46c71 src/ZF/AC/AC16_WO4.thy
--- a/src/ZF/AC/AC16_WO4.thy	Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/AC16_WO4.thy	Fri Jul 25 07:35:53 2008 +0200
@@ -7,7 +7,9 @@
 Tidied (using locales) by LCP
 *)
 
-theory AC16_WO4 imports AC16_lemmas begin
+theory AC16_WO4
+imports AC16_lemmas
+begin
 
 (* ********************************************************************** *)
 (* The case of finite set                                                 *)
@@ -202,8 +204,7 @@
 by (blast intro: eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans] 
                  succ_lepoll_natE)
 
-
-locale (open) AC16 =
+locale AC16 =
   fixes x and y and k and l and m and t_n and R and MM and LL and GG and s 
   defines k_def:     "k   == succ(l)"
       and MM_def:    "MM  == {v \<in> t_n. succ(k) \<lesssim> v Int y}"
@@ -558,9 +559,11 @@
 (* The main theorem AC16(n, k) ==> WO4(n-k)                               *)
 (* ********************************************************************** *)
 
+term AC16
+
 theorem AC16_WO4: 
-     "[| AC16(k #+ m, k); 0 < k; 0 < m; k \<in> nat; m \<in> nat |] ==> WO4(m)"
-apply (unfold AC16_def WO4_def)
+     "[| AC_Equiv.AC16(k #+ m, k); 0 < k; 0 < m; k \<in> nat; m \<in> nat |] ==> WO4(m)"
+apply (unfold AC_Equiv.AC16_def WO4_def)
 apply (rule allI)
 apply (case_tac "Finite (A)")
 apply (rule lemma1, assumption+)
@@ -569,7 +572,7 @@
 apply (erule_tac x = "A Un y" in allE)
 apply (frule infinite_Un, drule mp, assumption)
 apply (erule zero_lt_natE, assumption, clarify)
-apply (blast intro: AC16.conclusion) 
+apply (blast intro: AC16.conclusion [OF AC16.intro])
 done
 
 end
diff -r 646ea25ff59d -r 85ea2be46c71 src/ZF/AC/AC16_lemmas.thy
--- a/src/ZF/AC/AC16_lemmas.thy	Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/AC16_lemmas.thy	Fri Jul 25 07:35:53 2008 +0200
@@ -5,7 +5,9 @@
 Lemmas used in the proofs concerning AC16
 *)
 
-theory AC16_lemmas imports AC_Equiv Hartog Cardinal_aux begin
+theory AC16_lemmas
+imports AC_Equiv Hartog Cardinal_aux
+begin
 
 lemma cons_Diff_eq: "a\<notin>A ==> cons(a,A)-{a}=A"
 by fast
diff -r 646ea25ff59d -r 85ea2be46c71 src/ZF/AC/AC17_AC1.thy
--- a/src/ZF/AC/AC17_AC1.thy	Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/AC17_AC1.thy	Fri Jul 25 07:35:53 2008 +0200
@@ -8,7 +8,9 @@
 to AC0 and AC1.
 *)
 
-theory AC17_AC1 imports HH begin
+theory AC17_AC1
+imports HH
+begin
 
 
 (** AC0 is equivalent to AC1.  
diff -r 646ea25ff59d -r 85ea2be46c71 src/ZF/AC/AC18_AC19.thy
--- a/src/ZF/AC/AC18_AC19.thy	Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/AC18_AC19.thy	Fri Jul 25 07:35:53 2008 +0200
@@ -5,7 +5,9 @@
 The proof of AC1 ==> AC18 ==> AC19 ==> AC1
 *)
 
-theory AC18_AC19 imports AC_Equiv begin
+theory AC18_AC19
+imports AC_Equiv
+begin
 
 definition
   uu    :: "i => i" where
diff -r 646ea25ff59d -r 85ea2be46c71 src/ZF/AC/AC7_AC9.thy
--- a/src/ZF/AC/AC7_AC9.thy	Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/AC7_AC9.thy	Fri Jul 25 07:35:53 2008 +0200
@@ -6,7 +6,9 @@
 instances of AC.
 *)
 
-theory AC7_AC9 imports AC_Equiv begin
+theory AC7_AC9
+imports AC_Equiv
+begin
 
 (* ********************************************************************** *)
 (* Lemmas used in the proofs AC7 ==> AC6 and AC9 ==> AC1                  *)
diff -r 646ea25ff59d -r 85ea2be46c71 src/ZF/AC/AC_Equiv.thy
--- a/src/ZF/AC/AC_Equiv.thy	Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/AC_Equiv.thy	Fri Jul 25 07:35:53 2008 +0200
@@ -12,7 +12,9 @@
 but slightly changed.
 *)
 
-theory AC_Equiv imports Main begin (*obviously not Main_ZFC*)
+theory AC_Equiv
+imports Main
+begin (*obviously not Main_ZFC*)
 
 (* Well Ordering Theorems *)
 
diff -r 646ea25ff59d -r 85ea2be46c71 src/ZF/AC/DC.thy
--- a/src/ZF/AC/DC.thy	Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/DC.thy	Fri Jul 25 07:35:53 2008 +0200
@@ -5,7 +5,9 @@
 The proofs concerning the Axiom of Dependent Choice
 *)
 
-theory DC imports AC_Equiv Hartog Cardinal_aux begin
+theory DC
+imports AC_Equiv Hartog Cardinal_aux
+begin
 
 lemma RepFun_lepoll: "Ord(a) ==> {P(b). b \<in> a} \<lesssim> a"
 apply (unfold lepoll_def)
@@ -95,7 +97,7 @@
 	   transrec(b, %c r. THE x. first(x, {x \<in> X. <r``c, x> \<in> R}, Q))"
 
 
-locale (open) DC0_imp =
+locale DC0_imp =
   fixes XX and RR and X and R
 
   assumes all_ex: "\<forall>Y \<in> Pow(X). Y \<prec> nat --> (\<exists>x \<in> X. <Y, x> \<in> R)"
@@ -237,16 +239,16 @@
 apply (elim allE)
 apply (erule impE)
    (*these three results comprise Lemma 1*)
-apply (blast intro!: DC0_imp.lemma1_1 DC0_imp.lemma1_2 DC0_imp.lemma1_3)
+apply (blast intro!: DC0_imp.lemma1_1 [OF DC0_imp.intro] DC0_imp.lemma1_2 [OF DC0_imp.intro] DC0_imp.lemma1_3 [OF DC0_imp.intro])
 apply (erule bexE)
 apply (rule_tac x = "\<lambda>n \<in> nat. f`succ (n) `n" in rev_bexI)
- apply (rule lam_type, blast dest!: DC0_imp.lemma2 intro: fun_weaken_type)
+ apply (rule lam_type, blast dest!: DC0_imp.lemma2 [OF DC0_imp.intro] intro: fun_weaken_type)
 apply (rule oallI)
-apply (frule DC0_imp.lemma2, assumption)
+apply (frule DC0_imp.lemma2 [OF DC0_imp.intro], assumption)
   apply (blast intro: fun_weaken_type)
  apply (erule ltD) 
 (** LEVEL 11: last subgoal **)
-apply (subst DC0_imp.lemma3, assumption+) 
+apply (subst DC0_imp.lemma3 [OF DC0_imp.intro], assumption+) 
   apply (fast elim!: fun_weaken_type)
  apply (erule ltD) 
 apply (force simp add: lt_def) 
@@ -293,7 +295,7 @@
 done
 
 
-locale (open) imp_DC0 =
+locale imp_DC0 =
   fixes XX and RR and x and R and f and allRR
   defines XX_def: "XX == (\<Union>n \<in> nat.
 		      {f \<in> succ(n)->domain(R). \<forall>k \<in> n. <f`k, f`succ(k)> \<in> R})"
diff -r 646ea25ff59d -r 85ea2be46c71 src/ZF/AC/HH.thy
--- a/src/ZF/AC/HH.thy	Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/HH.thy	Fri Jul 25 07:35:53 2008 +0200
@@ -8,7 +8,9 @@
   AC15 ==> WO6
 *)
 
-theory HH imports AC_Equiv Hartog begin
+theory HH
+imports AC_Equiv Hartog
+begin
 
 definition
   HH :: "[i, i, i] => i"  where
diff -r 646ea25ff59d -r 85ea2be46c71 src/ZF/AC/Hartog.thy
--- a/src/ZF/AC/Hartog.thy	Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/Hartog.thy	Fri Jul 25 07:35:53 2008 +0200
@@ -5,7 +5,9 @@
 Hartog's function.
 *)
 
-theory Hartog imports AC_Equiv begin
+theory Hartog
+imports AC_Equiv
+begin
 
 definition
   Hartog :: "i => i"  where
diff -r 646ea25ff59d -r 85ea2be46c71 src/ZF/AC/WO1_AC.thy
--- a/src/ZF/AC/WO1_AC.thy	Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/WO1_AC.thy	Fri Jul 25 07:35:53 2008 +0200
@@ -25,7 +25,9 @@
 
 *)
 
-theory WO1_AC imports AC_Equiv begin
+theory WO1_AC
+imports AC_Equiv
+begin
 
 (* ********************************************************************** *)
 (* WO1 ==> AC1                                                            *)
diff -r 646ea25ff59d -r 85ea2be46c71 src/ZF/AC/WO1_WO7.thy
--- a/src/ZF/AC/WO1_WO7.thy	Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/WO1_WO7.thy	Fri Jul 25 07:35:53 2008 +0200
@@ -9,7 +9,9 @@
 Also, WO1 <-> WO8
 *)
 
-theory WO1_WO7 imports AC_Equiv begin
+theory WO1_WO7
+imports AC_Equiv
+begin
 
 definition
     "LEMMA ==
diff -r 646ea25ff59d -r 85ea2be46c71 src/ZF/AC/WO6_WO1.thy
--- a/src/ZF/AC/WO6_WO1.thy	Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/WO6_WO1.thy	Fri Jul 25 07:35:53 2008 +0200
@@ -11,7 +11,9 @@
 Fortunately order types made this proof also very easy.
 *)
 
-theory WO6_WO1 imports Cardinal_aux begin
+theory WO6_WO1
+imports Cardinal_aux
+begin
 
 (* Auxiliary definitions used in proof *)
 definition