# HG changeset patch
# User wenzelm
# Date 1027541755 -7200
# Node ID 8fcdf4a26468d4905d729ef75aab8f3bf3cef09b
# Parent  39fca1e5818a7d5929f3594bccf3d3c4c70ef48f
simplified locale predicates;

diff -r 39fca1e5818a -r 8fcdf4a26468 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Jul 24 22:14:42 2002 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Jul 24 22:15:55 2002 +0200
@@ -31,7 +31,8 @@
     P {} ==> (!!F x. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F"
   -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
 proof -
-  assume "P {}" and insert: "!!F x. finite F ==> x \<notin> F ==> P F ==> P (insert x F)"
+  assume "P {}" and
+    insert: "!!F x. finite F ==> x \<notin> F ==> P F ==> P (insert x F)"
   assume "finite F"
   thus "P F"
   proof induct
@@ -54,7 +55,8 @@
     P {} ==> (!!F a. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)) ==>
     P F"
 proof -
-  assume "P {}" and insert: "!!F a. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
+  assume "P {}" and insert:
+    "!!F a. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
   assume "finite F"
   thus "F \<subseteq> A ==> P F"
   proof induct
@@ -721,7 +723,7 @@
   apply (induct set: Finites)
    apply simp
   apply (simp add: AC insert_absorb Int_insert_left
-    LC.fold_insert [OF LC.intro, OF LC_axioms.intro])
+    LC.fold_insert [OF LC.intro])
   done
 
 lemma (in ACe) fold_Un_disjoint:
@@ -746,14 +748,14 @@
       by simp
     also have "... = (f \<circ> g) x (fold (f \<circ> g) e (F \<union> B))"
       by (rule LC.fold_insert [OF LC.intro])
-        (insert b insert, auto simp add: left_commute intro: LC_axioms.intro)
+        (insert b insert, auto simp add: left_commute)
     also from insert have "fold (f \<circ> g) e (F \<union> B) =
       fold (f \<circ> g) e F \<cdot> fold (f \<circ> g) e B" by blast
     also have "(f \<circ> g) x ... = (f \<circ> g) x (fold (f \<circ> g) e F) \<cdot> fold (f \<circ> g) e B"
       by (simp add: AC)
     also have "(f \<circ> g) x (fold (f \<circ> g) e F) = fold (f \<circ> g) e (insert x F)"
       by (rule LC.fold_insert [OF LC.intro, symmetric]) (insert b insert,
-	auto simp add: left_commute intro: LC_axioms.intro)
+	auto simp add: left_commute)
     finally show ?case .
   qed
 qed
@@ -779,7 +781,7 @@
 lemma setsum_insert [simp]:
     "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
   by (simp add: setsum_def
-    LC.fold_insert [OF LC.intro, OF LC_axioms.intro] plus_ac0_left_commute)
+    LC.fold_insert [OF LC.intro] plus_ac0_left_commute)
 
 lemma setsum_0: "setsum (\<lambda>i. 0) A = 0"
   apply (case_tac "finite A")
@@ -936,7 +938,8 @@
    apply (simp add: card_s_0_eq_empty)
   apply atomize
   apply (rotate_tac -1, erule finite_induct)
-   apply (simp_all (no_asm_simp) cong add: conj_cong add: card_s_0_eq_empty choose_deconstruct)
+   apply (simp_all (no_asm_simp) cong add: conj_cong
+     add: card_s_0_eq_empty choose_deconstruct)
   apply (subst card_Un_disjoint)
      prefer 4 apply (force simp add: constr_bij)
     prefer 3 apply force
@@ -945,7 +948,8 @@
   apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
   done
 
-theorem n_subsets: "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
+theorem n_subsets:
+    "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
   by (simp add: n_sub_lemma)
 
 end
diff -r 39fca1e5818a -r 8fcdf4a26468 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Jul 24 22:14:42 2002 +0200
+++ b/src/HOL/HOL.thy	Wed Jul 24 22:15:55 2002 +0200
@@ -344,7 +344,7 @@
     "!!P. (ALL x. x=t --> P(x)) = P(t)"
     "!!P. (ALL x. t=x --> P(x)) = P(t)"
   by (blast, blast, blast, blast, blast, rules+)
- 
+
 lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P --> Q) = (P' --> Q'))"
   by rules
 
@@ -605,14 +605,9 @@
   fixes f
   assumes mono: "A <= B ==> f A <= f B"
 
-lemmas monoI [intro?] = mono.intro [OF mono_axioms.intro]
+lemmas monoI [intro?] = mono.intro
   and monoD [dest?] = mono.mono
 
-lemma mono_def: "mono f == ALL A B. A <= B --> f A <= f B"
-  -- compatibility
-  by (simp only: atomize_eq mono_def mono_axioms_def)
-
-
 constdefs
   min :: "['a::ord, 'a] => 'a"
   "min a b == (if a <= b then a else b)"
diff -r 39fca1e5818a -r 8fcdf4a26468 src/HOL/NumberTheory/IntFact.thy
--- a/src/HOL/NumberTheory/IntFact.thy	Wed Jul 24 22:14:42 2002 +0200
+++ b/src/HOL/NumberTheory/IntFact.thy	Wed Jul 24 22:15:55 2002 +0200
@@ -39,7 +39,7 @@
 
 lemma setprod_insert [simp]:
     "finite A ==> a \<notin> A ==> setprod (insert a A) = a * setprod A"
-  by (simp add: setprod_def zmult_left_commute LC.fold_insert [OF LC.intro, OF LC_axioms.intro])
+  by (simp add: setprod_def zmult_left_commute LC.fold_insert [OF LC.intro])
 
 text {*
   \medskip @{term d22set} --- recursively defined set including all
diff -r 39fca1e5818a -r 8fcdf4a26468 src/HOL/Record.thy
--- a/src/HOL/Record.thy	Wed Jul 24 22:14:42 2002 +0200
+++ b/src/HOL/Record.thy	Wed Jul 24 22:15:55 2002 +0200
@@ -18,9 +18,6 @@
     and dest1: "dest1 == (\<lambda>p. fst (Rep p))"
     and dest2: "dest2 == (\<lambda>p. snd (Rep p))"
 
-lemmas product_typeI =
-  product_type.intro [OF product_type_axioms.intro]
-
 lemma (in product_type)
     "inject": "(pair x y = pair x' y') = (x = x' \<and> y = y')"
   by (simp add: pair type_definition.Abs_inject [OF "typedef"])
diff -r 39fca1e5818a -r 8fcdf4a26468 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Jul 24 22:14:42 2002 +0200
+++ b/src/HOL/Set.thy	Wed Jul 24 22:15:55 2002 +0200
@@ -960,16 +960,16 @@
 
 text {* \medskip Monotonicity. *}
 
-lemma mono_Un: "mono f ==> f A \<union> f B \<subseteq> f (A \<union> B)"
+lemma mono_Un: includes mono shows "f A \<union> f B \<subseteq> f (A \<union> B)"
   apply (rule Un_least)
-   apply (erule Un_upper1 [THEN [2] monoD])
-  apply (erule Un_upper2 [THEN [2] monoD])
+   apply (rule Un_upper1 [THEN mono])
+  apply (rule Un_upper2 [THEN mono])
   done
 
-lemma mono_Int: "mono f ==> f (A \<inter> B) \<subseteq> f A \<inter> f B"
+lemma mono_Int: includes mono shows "f (A \<inter> B) \<subseteq> f A \<inter> f B"
   apply (rule Int_greatest)
-   apply (erule Int_lower1 [THEN [2] monoD])
-  apply (erule Int_lower2 [THEN [2] monoD])
+   apply (rule Int_lower1 [THEN mono])
+  apply (rule Int_lower2 [THEN mono])
   done
 
 
diff -r 39fca1e5818a -r 8fcdf4a26468 src/HOL/Typedef.thy
--- a/src/HOL/Typedef.thy	Wed Jul 24 22:14:42 2002 +0200
+++ b/src/HOL/Typedef.thy	Wed Jul 24 22:15:55 2002 +0200
@@ -15,9 +15,6 @@
     and Abs_inverse: "y \<in> A ==> Rep (Abs y) = y"
   -- {* This will be axiomatized for each typedef! *}
 
-lemmas type_definitionI [intro] =
-  type_definition.intro [OF type_definition_axioms.intro]
-
 lemma (in type_definition) Rep_inject:
   "(Rep x = Rep y) = (x = y)"
 proof
diff -r 39fca1e5818a -r 8fcdf4a26468 src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Wed Jul 24 22:14:42 2002 +0200
+++ b/src/HOL/Unix/Unix.thy	Wed Jul 24 22:15:55 2002 +0200
@@ -1131,7 +1131,7 @@
 text {*
   So this is our final result:
 
-  @{thm [display] result [OF situation_axioms.intro, no_vars]}
+  @{thm [display] result [OF situation.intro, no_vars]}
 *}
 
 end
diff -r 39fca1e5818a -r 8fcdf4a26468 src/ZF/AC/AC18_AC19.thy
--- a/src/ZF/AC/AC18_AC19.thy	Wed Jul 24 22:14:42 2002 +0200
+++ b/src/ZF/AC/AC18_AC19.thy	Wed Jul 24 22:15:55 2002 +0200
@@ -36,7 +36,7 @@
 
 lemma AC1_AC18: "AC1 ==> PROP AC18"
 apply (unfold AC1_def)
-apply (rule AC18.intro [OF AC18_axioms.intro])
+apply (rule AC18.intro)
 apply (fast elim!: lemma_AC18 apply_type intro!: equalityI INT_I UN_I)
 done