# HG changeset patch
# User ballarin
# Date 1068124685 -3600
# Node ID 342634f38451edb5d2e059b1007a51713f8d0560
# Parent  91a64a93bdb46e36864cddbc11950637d51d2772
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
default.

diff -r 91a64a93bdb4 -r 342634f38451 NEWS
--- a/NEWS	Fri Oct 31 06:54:22 2003 +0100
+++ b/NEWS	Thu Nov 06 14:18:05 2003 +0100
@@ -48,6 +48,8 @@
     Resolve particular premise with <locale>.intro to obtain old form.
   - Fixed bug in type inference ("unify_frozen") that prevented mix of target
     specification and "includes" elements in goal statement.
+  - Rule sets <locale>.intro and <locale>.axioms no longer declared as
+    [intro?] and [elim?] (respectively) by default.
 
 * HOL: Tactic emulation methods induct_tac and case_tac understand static
   (Isar) contexts.
diff -r 91a64a93bdb4 -r 342634f38451 src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Fri Oct 31 06:54:22 2003 +0100
+++ b/src/HOL/Algebra/Coset.thy	Thu Nov 06 14:18:05 2003 +0100
@@ -46,7 +46,7 @@
 *}
 lemma (in group) is_coset:
   "coset G"
-  ..
+  by (rule coset.intro)
 
 text{*Lemmas useful for Sylow's Theorem*}
 
diff -r 91a64a93bdb4 -r 342634f38451 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Fri Oct 31 06:54:22 2003 +0100
+++ b/src/HOL/Algebra/Group.thy	Thu Nov 06 14:18:05 2003 +0100
@@ -415,7 +415,7 @@
 lemma (in subgroup) group_axiomsI [intro]:
   includes group G
   shows "group_axioms (G(| carrier := H |))"
-  by rule (auto intro: l_inv r_inv simp add: Units_def)
+  by (rule group_axioms.intro) (auto intro: l_inv r_inv simp add: Units_def)
 
 lemma (in subgroup) groupI [intro]:
   includes group G
@@ -440,8 +440,8 @@
     and inv: "!!a. a \<in> H ==> inv a \<in> H"
     and mult: "!!a b. [|a \<in> H; b \<in> H|] ==> a \<otimes> b \<in> H"
   shows "subgroup H G"
-proof
-  from subset and mult show "submagma H G" ..
+proof (rule subgroup.intro)
+  from subset and mult show "submagma H G" by (rule submagma.intro)
 next
   have "\<one> \<in> H" by (rule one_in_subset) (auto simp only: prems)
   with inv show "subgroup_axioms H G"
@@ -472,7 +472,7 @@
 lemma (in subgroup) finite_imp_card_positive:
   "finite (carrier G) ==> 0 < card H"
 proof (rule classical)
-  have sub: "subgroup H G" using prems ..
+  have sub: "subgroup H G" using prems by (rule subgroup.intro)
   assume fin: "finite (carrier G)"
     and zero: "~ 0 < card H"
   then have "finite H" by (blast intro: finite_subset dest: subset)
@@ -505,12 +505,13 @@
 lemma DirProdSemigroup_magma:
   includes magma G + magma H
   shows "magma (G \<times>\<^sub>s H)"
-  by rule (auto simp add: DirProdSemigroup_def)
+  by (rule magma.intro) (auto simp add: DirProdSemigroup_def)
 
 lemma DirProdSemigroup_semigroup_axioms:
   includes semigroup G + semigroup H
   shows "semigroup_axioms (G \<times>\<^sub>s H)"
-  by rule (auto simp add: DirProdSemigroup_def G.m_assoc H.m_assoc)
+  by (rule semigroup_axioms.intro)
+    (auto simp add: DirProdSemigroup_def G.m_assoc H.m_assoc)
 
 lemma DirProdSemigroup_semigroup:
   includes semigroup G + semigroup H
@@ -522,13 +523,13 @@
 lemma DirProdGroup_magma:
   includes magma G + magma H
   shows "magma (G \<times>\<^sub>g H)"
-  by rule
+  by (rule magma.intro)
     (auto simp add: DirProdGroup_def DirProdSemigroup_def)
 
 lemma DirProdGroup_semigroup_axioms:
   includes semigroup G + semigroup H
   shows "semigroup_axioms (G \<times>\<^sub>g H)"
-  by rule
+  by (rule semigroup_axioms.intro)
     (auto simp add: DirProdGroup_def DirProdSemigroup_def
       G.m_assoc H.m_assoc)
 
@@ -581,12 +582,12 @@
 lemma (in semigroup) hom:
   includes semigroup G
   shows "semigroup (| carrier = hom G G, mult = op o |)"
-proof
+proof (rule semigroup.intro)
   show "magma (| carrier = hom G G, mult = op o |)"
-    by rule (simp add: Pi_def hom_def)
+    by (rule magma.intro) (simp add: Pi_def hom_def)
 next
   show "semigroup_axioms (| carrier = hom G G, mult = op o |)"
-    by rule (simp add: o_assoc)
+    by (rule semigroup_axioms.intro) (simp add: o_assoc)
 qed
 
 lemma hom_mult:
diff -r 91a64a93bdb4 -r 342634f38451 src/HOL/Real/HahnBanach/FunctionNorm.thy
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Fri Oct 31 06:54:22 2003 +0100
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Thu Nov 06 14:18:05 2003 +0100
@@ -23,6 +23,8 @@
 locale continuous = var V + norm_syntax + linearform +
   assumes bounded: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
 
+declare continuous.intro [intro?] continuous_axioms.intro [intro?]
+
 lemma continuousI [intro]:
   includes norm_syntax + linearform
   assumes r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
diff -r 91a64a93bdb4 -r 342634f38451 src/HOL/Real/HahnBanach/Linearform.thy
--- a/src/HOL/Real/HahnBanach/Linearform.thy	Fri Oct 31 06:54:22 2003 +0100
+++ b/src/HOL/Real/HahnBanach/Linearform.thy	Thu Nov 06 14:18:05 2003 +0100
@@ -16,6 +16,8 @@
   assumes add [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y"
     and mult [iff]: "x \<in> V \<Longrightarrow> f (a \<cdot> x) = a * f x"
 
+declare linearform.intro [intro?]
+
 lemma (in linearform) neg [iff]:
   includes vectorspace
   shows "x \<in> V \<Longrightarrow> f (- x) = - f x"
diff -r 91a64a93bdb4 -r 342634f38451 src/HOL/Real/HahnBanach/NormedSpace.thy
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Fri Oct 31 06:54:22 2003 +0100
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Thu Nov 06 14:18:05 2003 +0100
@@ -23,6 +23,8 @@
     and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
     and subadditive [iff?]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
 
+declare seminorm.intro [intro?]
+
 lemma (in seminorm) diff_subadditive:
   includes vectorspace
   shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
@@ -71,6 +73,8 @@
 
 locale normed_vectorspace = vectorspace + norm
 
+declare normed_vectorspace.intro [intro?]
+
 lemma (in normed_vectorspace) gt_zero [intro?]:
   "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> 0 < \<parallel>x\<parallel>"
 proof -
diff -r 91a64a93bdb4 -r 342634f38451 src/HOL/Real/HahnBanach/Subspace.thy
--- a/src/HOL/Real/HahnBanach/Subspace.thy	Fri Oct 31 06:54:22 2003 +0100
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Thu Nov 06 14:18:05 2003 +0100
@@ -22,6 +22,8 @@
     and add_closed [iff]: "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x + y \<in> U"
     and mult_closed [iff]: "x \<in> U \<Longrightarrow> a \<cdot> x \<in> U"
 
+declare vectorspace.intro [intro?] subspace.intro [intro?]
+
 syntax (symbols)
   subspace :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"    (infix "\<unlhd>" 50)
 
diff -r 91a64a93bdb4 -r 342634f38451 src/HOL/ex/Locales.thy
--- a/src/HOL/ex/Locales.thy	Fri Oct 31 06:54:22 2003 +0100
+++ b/src/HOL/ex/Locales.thy	Thu Nov 06 14:18:05 2003 +0100
@@ -321,6 +321,9 @@
   assumes left_inv: "x\<inv> \<cdot> x = \<one>"
     and left_one: "\<one> \<cdot> x = x"
 
+declare semigroup.intro [intro?]
+  group.intro [intro?] group_axioms.intro [intro?]
+
 text {*
   Note that we prefer to call the @{text group} record structure
   @{text G} rather than @{text S} inherited from @{text semigroup}.
diff -r 91a64a93bdb4 -r 342634f38451 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Oct 31 06:54:22 2003 +0100
+++ b/src/Pure/Isar/locale.ML	Thu Nov 06 14:18:05 2003 +0100
@@ -887,17 +887,6 @@
     val ((import_ctxt, axioms'), (import_elemss, _)) =
       activate_facts prep_facts ((context, axioms), ps);
 
-(* CB: testing *)
-(*
-val axioms' = if true (* null axioms *) then axioms' else
-let val {view = (ax3_view, ax3_axioms), ...} =
-  the_locale (ProofContext.theory_of context) "Type.ax3";
-val ax_TrueFalse = Thm.assume (read_cterm (sign_of_thm (hd axioms))
-  ("True <-> False", propT));
-val {view = (ax4_view, ax4_axioms), ...} =
-  the_locale (ProofContext.theory_of context) "Type.ax4";
-in axioms' @ ax3_axioms @ [ax_TrueFalse] @ (tl ax4_axioms) end;
-*)
     val ((ctxt, _), (elemss, _)) =
       activate_facts prep_facts ((import_ctxt, axioms'), qs);
   in
@@ -1126,7 +1115,7 @@
             [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, ([], []))])]])];
         in
           def_thy |> have_thmss_qualified "" aname
-            [((introN, [ContextRules.intro_query_global None]), [([intro], [])])]
+            [((introN, []), [([intro], [])])]
           |> #1 |> rpair (elemss', [statement])
         end;
     val (thy'', view) =
@@ -1138,8 +1127,8 @@
           val cstatement = Thm.cterm_of (Theory.sign_of def_thy) statement;
         in
           def_thy |> have_thmss_qualified "" bname
-            [((introN, [ContextRules.intro_query_global None]), [([intro], [])]),
-             ((axiomsN, [ContextRules.elim_query_global None]), [(map Drule.standard axioms, [])])]
+            [((introN, []), [([intro], [])]),
+             ((axiomsN, []), [(map Drule.standard axioms, [])])]
           |> #1 |> rpair ([cstatement], axioms)
         end;
   in (thy'', (elemss', view)) end;