--- a/src/HOL/Bali/TypeSafe.thy Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/Bali/TypeSafe.thy Tue May 04 08:55:43 2010 +0200
@@ -9,8 +9,6 @@
section "error free"
-hide_const field
-
lemma error_free_halloc:
assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
error_free_s0: "error_free s0"
--- a/src/HOL/Big_Operators.thy Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/Big_Operators.thy Tue May 04 08:55:43 2010 +0200
@@ -33,7 +33,7 @@
text {* for ad-hoc proofs for @{const fold_image} *}
lemma (in comm_monoid_add) comm_monoid_mult:
- "comm_monoid_mult (op +) 0"
+ "class.comm_monoid_mult (op +) 0"
proof qed (auto intro: add_assoc add_commute)
notation times (infixl "*" 70)
@@ -1200,7 +1200,8 @@
context semilattice_inf
begin
-lemma ab_semigroup_idem_mult_inf: "ab_semigroup_idem_mult inf"
+lemma ab_semigroup_idem_mult_inf:
+ "class.ab_semigroup_idem_mult inf"
proof qed (rule inf_assoc inf_commute inf_idem)+
lemma fold_inf_insert[simp]: "finite A \<Longrightarrow> fold inf b (insert a A) = inf a (fold inf b A)"
@@ -1270,7 +1271,7 @@
context semilattice_sup
begin
-lemma ab_semigroup_idem_mult_sup: "ab_semigroup_idem_mult sup"
+lemma ab_semigroup_idem_mult_sup: "class.ab_semigroup_idem_mult sup"
by (rule semilattice_inf.ab_semigroup_idem_mult_inf)(rule dual_semilattice)
lemma fold_sup_insert[simp]: "finite A \<Longrightarrow> fold sup b (insert a A) = sup a (fold sup b A)"
@@ -1490,15 +1491,15 @@
using assms by (rule Max.hom_commute)
lemma ab_semigroup_idem_mult_min:
- "ab_semigroup_idem_mult min"
+ "class.ab_semigroup_idem_mult min"
proof qed (auto simp add: min_def)
lemma ab_semigroup_idem_mult_max:
- "ab_semigroup_idem_mult max"
+ "class.ab_semigroup_idem_mult max"
proof qed (auto simp add: max_def)
lemma max_lattice:
- "semilattice_inf (op \<ge>) (op >) max"
+ "class.semilattice_inf (op \<ge>) (op >) max"
by (fact min_max.dual_semilattice)
lemma dual_max:
--- a/src/HOL/Complete_Lattice.thy Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/Complete_Lattice.thy Tue May 04 08:55:43 2010 +0200
@@ -33,8 +33,8 @@
begin
lemma dual_complete_lattice:
- "complete_lattice Sup Inf (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
- by (auto intro!: complete_lattice.intro dual_bounded_lattice)
+ "class.complete_lattice Sup Inf (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
+ by (auto intro!: class.complete_lattice.intro dual_bounded_lattice)
(unfold_locales, (fact bot_least top_greatest
Sup_upper Sup_least Inf_lower Inf_greatest)+)
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Tue May 04 08:55:43 2010 +0200
@@ -265,7 +265,7 @@
lemmas dlo_simps[no_atp] = order_refl less_irrefl not_less not_le exists_neq
le_less neq_iff linear less_not_permute
-lemma axiom[no_atp]: "dense_linorder (op \<le>) (op <)" by (rule dense_linorder_axioms)
+lemma axiom[no_atp]: "class.dense_linorder (op \<le>) (op <)" by (rule dense_linorder_axioms)
lemma atoms[no_atp]:
shows "TERM (less :: 'a \<Rightarrow> _)"
and "TERM (less_eq :: 'a \<Rightarrow> _)"
--- a/src/HOL/Finite_Set.thy Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/Finite_Set.thy Tue May 04 08:55:43 2010 +0200
@@ -509,13 +509,8 @@
subsection {* Class @{text finite} *}
-setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
class finite =
assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
-setup {* Sign.parent_path *}
-hide_const finite
-
-context finite
begin
lemma finite [simp]: "finite (A \<Colon> 'a set)"
--- a/src/HOL/HOL.thy Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/HOL.thy Tue May 04 08:55:43 2010 +0200
@@ -1886,7 +1886,6 @@
*}
hide_const (open) eq
-hide_const eq
text {* Cases *}
--- a/src/HOL/Lattices.thy Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/Lattices.thy Tue May 04 08:55:43 2010 +0200
@@ -67,8 +67,8 @@
text {* Dual lattice *}
lemma dual_semilattice:
- "semilattice_inf (op \<ge>) (op >) sup"
-by (rule semilattice_inf.intro, rule dual_order)
+ "class.semilattice_inf (op \<ge>) (op >) sup"
+by (rule class.semilattice_inf.intro, rule dual_order)
(unfold_locales, simp_all add: sup_least)
end
@@ -235,8 +235,8 @@
begin
lemma dual_lattice:
- "lattice (op \<ge>) (op >) sup inf"
- by (rule lattice.intro, rule dual_semilattice, rule semilattice_sup.intro, rule dual_order)
+ "class.lattice (op \<ge>) (op >) sup inf"
+ by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order)
(unfold_locales, auto)
lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
@@ -347,8 +347,8 @@
by(simp add: inf_sup_aci inf_sup_distrib1)
lemma dual_distrib_lattice:
- "distrib_lattice (op \<ge>) (op >) sup inf"
- by (rule distrib_lattice.intro, rule dual_lattice)
+ "class.distrib_lattice (op \<ge>) (op >) sup inf"
+ by (rule class.distrib_lattice.intro, rule dual_lattice)
(unfold_locales, fact inf_sup_distrib1)
lemmas sup_inf_distrib =
@@ -419,7 +419,7 @@
begin
lemma dual_bounded_lattice:
- "bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
+ "class.bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
by unfold_locales (auto simp add: less_le_not_le)
end
@@ -431,8 +431,8 @@
begin
lemma dual_boolean_algebra:
- "boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
- by (rule boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
+ "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
+ by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
(unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
lemma compl_inf_bot:
--- a/src/HOL/Library/Multiset.thy Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/Library/Multiset.thy Tue May 04 08:55:43 2010 +0200
@@ -1239,7 +1239,7 @@
qed
have trans: "\<And>K M N :: 'a multiset. K \<subset># M \<Longrightarrow> M \<subset># N \<Longrightarrow> K \<subset># N"
unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
- show "order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset" proof
+ show "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset" proof
qed (auto simp add: le_multiset_def irrefl dest: trans)
qed
--- a/src/HOL/Orderings.thy Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/Orderings.thy Tue May 04 08:55:43 2010 +0200
@@ -106,7 +106,7 @@
text {* Dual order *}
lemma dual_preorder:
- "preorder (op \<ge>) (op >)"
+ "class.preorder (op \<ge>) (op >)"
proof qed (auto simp add: less_le_not_le intro: order_trans)
end
@@ -186,7 +186,7 @@
text {* Dual order *}
lemma dual_order:
- "order (op \<ge>) (op >)"
+ "class.order (op \<ge>) (op >)"
by (intro_locales, rule dual_preorder) (unfold_locales, rule antisym)
end
@@ -257,8 +257,8 @@
text {* Dual order *}
lemma dual_linorder:
- "linorder (op \<ge>) (op >)"
-by (rule linorder.intro, rule dual_order) (unfold_locales, rule linear)
+ "class.linorder (op \<ge>) (op >)"
+by (rule class.linorder.intro, rule dual_order) (unfold_locales, rule linear)
text {* min/max *}
--- a/src/HOL/Wellfounded.thy Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/Wellfounded.thy Tue May 04 08:55:43 2010 +0200
@@ -68,7 +68,7 @@
assumes lin: "OFCLASS('a::ord, linorder_class)"
shows "OFCLASS('a::ord, wellorder_class)"
using lin by (rule wellorder_class.intro)
- (blast intro: wellorder_axioms.intro wf_induct_rule [OF wf])
+ (blast intro: class.wellorder_axioms.intro wf_induct_rule [OF wf])
lemma (in wellorder) wf:
"wf {(x, y). x < y}"
--- a/src/HOL/Word/WordArith.thy Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/Word/WordArith.thy Tue May 04 08:55:43 2010 +0200
@@ -17,7 +17,7 @@
by (auto simp del: word_uint.Rep_inject
simp: word_uint.Rep_inject [symmetric])
-lemma signed_linorder: "linorder word_sle word_sless"
+lemma signed_linorder: "class.linorder word_sle word_sless"
proof
qed (unfold word_sle_def word_sless_def, auto)
--- a/src/HOL/ex/Landau.thy Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/ex/Landau.thy Tue May 04 08:55:43 2010 +0200
@@ -187,7 +187,7 @@
proof -
interpret preorder_equiv less_eq_fun less_fun proof
qed (simp_all add: less_fun_def less_eq_fun_refl, auto intro: less_eq_fun_trans)
- show "preorder_equiv less_eq_fun less_fun" using preorder_equiv_axioms .
+ show "class.preorder_equiv less_eq_fun less_fun" using preorder_equiv_axioms .
show "preorder_equiv.equiv less_eq_fun = equiv_fun"
by (simp add: expand_fun_eq equiv_def equiv_fun_less_eq_fun)
qed
--- a/src/HOLCF/CompactBasis.thy Tue May 04 08:55:39 2010 +0200
+++ b/src/HOLCF/CompactBasis.thy Tue May 04 08:55:43 2010 +0200
@@ -237,12 +237,12 @@
where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
lemma fold_pd_PDUnit:
- assumes "ab_semigroup_idem_mult f"
+ assumes "class.ab_semigroup_idem_mult f"
shows "fold_pd g f (PDUnit x) = g x"
unfolding fold_pd_def Rep_PDUnit by simp
lemma fold_pd_PDPlus:
- assumes "ab_semigroup_idem_mult f"
+ assumes "class.ab_semigroup_idem_mult f"
shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
proof -
interpret ab_semigroup_idem_mult f by fact
--- a/src/HOLCF/ConvexPD.thy Tue May 04 08:55:39 2010 +0200
+++ b/src/HOLCF/ConvexPD.thy Tue May 04 08:55:43 2010 +0200
@@ -412,7 +412,7 @@
(\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
lemma ACI_convex_bind:
- "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
+ "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
apply unfold_locales
apply (simp add: convex_plus_assoc)
apply (simp add: convex_plus_commute)
--- a/src/HOLCF/LowerPD.thy Tue May 04 08:55:39 2010 +0200
+++ b/src/HOLCF/LowerPD.thy Tue May 04 08:55:43 2010 +0200
@@ -393,7 +393,7 @@
(\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
lemma ACI_lower_bind:
- "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
+ "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
apply unfold_locales
apply (simp add: lower_plus_assoc)
apply (simp add: lower_plus_commute)
--- a/src/HOLCF/UpperPD.thy Tue May 04 08:55:39 2010 +0200
+++ b/src/HOLCF/UpperPD.thy Tue May 04 08:55:43 2010 +0200
@@ -388,7 +388,7 @@
(\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
lemma ACI_upper_bind:
- "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
+ "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
apply unfold_locales
apply (simp add: upper_plus_assoc)
apply (simp add: upper_plus_commute)
--- a/src/Pure/Isar/class.ML Tue May 04 08:55:39 2010 +0200
+++ b/src/Pure/Isar/class.ML Tue May 04 08:55:43 2010 +0200
@@ -276,16 +276,16 @@
#> pair (param_map, params, assm_axiom)))
end;
-fun gen_class prep_class_spec bname raw_supclasses raw_elems thy =
+fun gen_class prep_class_spec b raw_supclasses raw_elems thy =
let
- val class = Sign.full_name thy bname;
+ val class = Sign.full_name thy b;
val (((sups, supparam_names), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
prep_class_spec thy raw_supclasses raw_elems;
in
thy
- |> Expression.add_locale bname Binding.empty supexpr elems
+ |> Expression.add_locale b (Binding.qualify true "class" b) supexpr elems
|> snd |> Local_Theory.exit_global
- |> adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax
+ |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax
||> Theory.checkpoint
|-> (fn (param_map, params, assm_axiom) =>
`(fn thy => calculate thy class sups base_sort param_map assm_axiom)