--- a/doc-src/Classes/Thy/Classes.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/doc-src/Classes/Thy/Classes.thy Thu Mar 26 20:08:55 2009 +0100
@@ -458,7 +458,7 @@
of monoids for lists:
*}
-interpretation %quote list_monoid!: monoid append "[]"
+interpretation %quote list_monoid: monoid append "[]"
proof qed auto
text {*
@@ -473,7 +473,7 @@
"replicate 0 _ = []"
| "replicate (Suc n) xs = xs @ replicate n xs"
-interpretation %quote list_monoid!: monoid append "[]" where
+interpretation %quote list_monoid: monoid append "[]" where
"monoid.pow_nat append [] = replicate"
proof -
interpret monoid append "[]" ..
--- a/doc-src/Classes/Thy/document/Classes.tex Thu Mar 26 19:24:21 2009 +0100
+++ b/doc-src/Classes/Thy/document/Classes.tex Thu Mar 26 20:08:55 2009 +0100
@@ -863,7 +863,7 @@
%
\isatagquote
\isacommand{interpretation}\isamarkupfalse%
-\ list{\isacharunderscore}monoid{\isacharbang}{\isacharcolon}\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ \isacommand{qed}\isamarkupfalse%
\ auto%
@@ -894,7 +894,7 @@
\ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{interpretation}\isamarkupfalse%
-\ list{\isacharunderscore}monoid{\isacharbang}{\isacharcolon}\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharminus}\isanewline
@@ -1191,7 +1191,7 @@
\hspace*{0pt}\\
\hspace*{0pt}pow{\char95}nat ::~forall a.~(Monoid a) => Nat -> a -> a;\\
\hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\
-\hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\
+\hspace*{0pt}pow{\char95}nat (Suc n) xa = mult xa (pow{\char95}nat n xa);\\
\hspace*{0pt}\\
\hspace*{0pt}pow{\char95}int ::~forall a.~(Group a) => Integer -> a -> a;\\
\hspace*{0pt}pow{\char95}int k x =\\
@@ -1272,8 +1272,8 @@
\hspace*{0pt} ~IntInf.int group;\\
\hspace*{0pt}\\
\hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\
-\hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) x =\\
-\hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) x (pow{\char95}nat A{\char95}~n x);\\
+\hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) xa =\\
+\hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) xa (pow{\char95}nat A{\char95}~n xa);\\
\hspace*{0pt}\\
\hspace*{0pt}fun pow{\char95}int A{\char95}~k x =\\
\hspace*{0pt} ~(if IntInf.<= ((0 :~IntInf.int),~k)\\
--- a/src/FOL/ex/LocaleTest.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/FOL/ex/LocaleTest.thy Thu Mar 26 20:08:55 2009 +0100
@@ -119,7 +119,7 @@
term extra_type.test thm extra_type.test_def
-interpretation var: extra_type "0" "%x y. x = 0" .
+interpretation var?: extra_type "0" "%x y. x = 0" .
thm var.test_def
@@ -381,13 +381,13 @@
subsection {* Sublocale, then interpretation in theory *}
-interpretation int: lgrp "op +" "0" "minus"
+interpretation int?: lgrp "op +" "0" "minus"
proof unfold_locales
qed (rule int_assoc int_zero int_minus)+
thm int.assoc int.semi_axioms
-interpretation int2: semi "op +"
+interpretation int2?: semi "op +"
by unfold_locales (* subsumed, thm int2.assoc not generated *)
thm int.lone int.right.rone
@@ -443,7 +443,7 @@
end
-interpretation x!: logic_o "op &" "Not"
+interpretation x: logic_o "op &" "Not"
where bool_logic_o: "logic_o.lor_o(op &, Not, x, y) <-> x | y"
proof -
show bool_logic_o: "PROP logic_o(op &, Not)" by unfold_locales fast+
--- a/src/HOL/Algebra/AbelCoset.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Algebra/AbelCoset.thy Thu Mar 26 20:08:55 2009 +0100
@@ -540,8 +540,8 @@
(| carrier = carrier H, mult = add H, one = zero H |) h"
shows "abelian_group_hom G H h"
proof -
- interpret G!: abelian_group G by fact
- interpret H!: abelian_group H by fact
+ interpret G: abelian_group G by fact
+ interpret H: abelian_group H by fact
show ?thesis apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
apply fact
apply fact
@@ -692,7 +692,7 @@
assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
shows "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
proof -
- interpret G!: ring G by fact
+ interpret G: ring G by fact
from carr
have "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)" by (rule a_rcos_module)
with carr
--- a/src/HOL/Algebra/Group.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Algebra/Group.thy Thu Mar 26 20:08:55 2009 +0100
@@ -488,8 +488,8 @@
assumes "monoid G" and "monoid H"
shows "monoid (G \<times>\<times> H)"
proof -
- interpret G!: monoid G by fact
- interpret H!: monoid H by fact
+ interpret G: monoid G by fact
+ interpret H: monoid H by fact
from assms
show ?thesis by (unfold monoid_def DirProd_def, auto)
qed
@@ -500,8 +500,8 @@
assumes "group G" and "group H"
shows "group (G \<times>\<times> H)"
proof -
- interpret G!: group G by fact
- interpret H!: group H by fact
+ interpret G: group G by fact
+ interpret H: group H by fact
show ?thesis by (rule groupI)
(auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
simp add: DirProd_def)
@@ -525,9 +525,9 @@
and h: "h \<in> carrier H"
shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
proof -
- interpret G!: group G by fact
- interpret H!: group H by fact
- interpret Prod!: group "G \<times>\<times> H"
+ interpret G: group G by fact
+ interpret H: group H by fact
+ interpret Prod: group "G \<times>\<times> H"
by (auto intro: DirProd_group group.intro group.axioms assms)
show ?thesis by (simp add: Prod.inv_equality g h)
qed
--- a/src/HOL/Algebra/Ideal.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Algebra/Ideal.thy Thu Mar 26 20:08:55 2009 +0100
@@ -711,7 +711,7 @@
obtains "carrier R = I"
| "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I"
proof -
- interpret R!: cring R by fact
+ interpret R: cring R by fact
assume "carrier R = I ==> thesis"
and "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I \<Longrightarrow> thesis"
then show thesis using primeidealCD [OF R.is_cring notprime] by blast
--- a/src/HOL/Algebra/IntRing.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Algebra/IntRing.thy Thu Mar 26 20:08:55 2009 +0100
@@ -96,7 +96,7 @@
interpretation needs to be done as early as possible --- that is,
with as few assumptions as possible. *}
-interpretation int!: monoid \<Z>
+interpretation int: monoid \<Z>
where "carrier \<Z> = UNIV"
and "mult \<Z> x y = x * y"
and "one \<Z> = 1"
@@ -104,7 +104,7 @@
proof -
-- "Specification"
show "monoid \<Z>" proof qed (auto simp: int_ring_def)
- then interpret int!: monoid \<Z> .
+ then interpret int: monoid \<Z> .
-- "Carrier"
show "carrier \<Z> = UNIV" by (simp add: int_ring_def)
@@ -116,12 +116,12 @@
show "pow \<Z> x n = x^n" by (induct n) (simp, simp add: int_ring_def)+
qed
-interpretation int!: comm_monoid \<Z>
+interpretation int: comm_monoid \<Z>
where "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
proof -
-- "Specification"
show "comm_monoid \<Z>" proof qed (auto simp: int_ring_def)
- then interpret int!: comm_monoid \<Z> .
+ then interpret int: comm_monoid \<Z> .
-- "Operations"
{ fix x y have "mult \<Z> x y = x * y" by (simp add: int_ring_def) }
@@ -139,14 +139,14 @@
qed
qed
-interpretation int!: abelian_monoid \<Z>
+interpretation int: abelian_monoid \<Z>
where "zero \<Z> = 0"
and "add \<Z> x y = x + y"
and "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
proof -
-- "Specification"
show "abelian_monoid \<Z>" proof qed (auto simp: int_ring_def)
- then interpret int!: abelian_monoid \<Z> .
+ then interpret int: abelian_monoid \<Z> .
-- "Operations"
{ fix x y show "add \<Z> x y = x + y" by (simp add: int_ring_def) }
@@ -164,7 +164,7 @@
qed
qed
-interpretation int!: abelian_group \<Z>
+interpretation int: abelian_group \<Z>
where "a_inv \<Z> x = - x"
and "a_minus \<Z> x y = x - y"
proof -
@@ -174,7 +174,7 @@
show "!!x. x \<in> carrier \<Z> ==> EX y : carrier \<Z>. y \<oplus>\<^bsub>\<Z>\<^esub> x = \<zero>\<^bsub>\<Z>\<^esub>"
by (simp add: int_ring_def) arith
qed (auto simp: int_ring_def)
- then interpret int!: abelian_group \<Z> .
+ then interpret int: abelian_group \<Z> .
-- "Operations"
{ fix x y have "add \<Z> x y = x + y" by (simp add: int_ring_def) }
@@ -187,7 +187,7 @@
show "a_minus \<Z> x y = x - y" by (simp add: int.minus_eq add a_inv)
qed
-interpretation int!: "domain" \<Z>
+interpretation int: "domain" \<Z>
proof qed (auto simp: int_ring_def left_distrib right_distrib)
@@ -203,7 +203,7 @@
"(True ==> PROP R) == PROP R"
by simp_all
-interpretation int! (* FIXME [unfolded UNIV] *) :
+interpretation int (* FIXME [unfolded UNIV] *) :
partial_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
where "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
and "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
@@ -219,7 +219,7 @@
by (simp add: lless_def) auto
qed
-interpretation int! (* FIXME [unfolded UNIV] *) :
+interpretation int (* FIXME [unfolded UNIV] *) :
lattice "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
where "join (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = max x y"
and "meet (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = min x y"
@@ -232,7 +232,7 @@
apply (simp add: greatest_def Lower_def)
apply arith
done
- then interpret int!: lattice "?Z" .
+ then interpret int: lattice "?Z" .
show "join ?Z x y = max x y"
apply (rule int.joinI)
apply (simp_all add: least_def Upper_def)
@@ -245,7 +245,7 @@
done
qed
-interpretation int! (* [unfolded UNIV] *) :
+interpretation int (* [unfolded UNIV] *) :
total_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
proof qed clarsimp
--- a/src/HOL/Algebra/RingHom.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Algebra/RingHom.thy Thu Mar 26 20:08:55 2009 +0100
@@ -61,8 +61,8 @@
assumes h: "h \<in> ring_hom R S"
shows "ring_hom_ring R S h"
proof -
- interpret R!: ring R by fact
- interpret S!: ring S by fact
+ interpret R: ring R by fact
+ interpret S: ring S by fact
show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
apply (rule R.is_ring)
apply (rule S.is_ring)
@@ -78,8 +78,8 @@
shows "ring_hom_ring R S h"
proof -
interpret abelian_group_hom R S h by fact
- interpret R!: ring R by fact
- interpret S!: ring S by fact
+ interpret R: ring R by fact
+ interpret S: ring S by fact
show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring)
apply (insert group_hom.homh[OF a_group_hom])
apply (unfold hom_def ring_hom_def, simp)
@@ -94,8 +94,8 @@
shows "ring_hom_cring R S h"
proof -
interpret ring_hom_ring R S h by fact
- interpret R!: cring R by fact
- interpret S!: cring S by fact
+ interpret R: cring R by fact
+ interpret S: cring S by fact
show ?thesis by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro)
(rule R.is_cring, rule S.is_cring, rule homh)
qed
--- a/src/HOL/Algebra/UnivPoly.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy Thu Mar 26 20:08:55 2009 +0100
@@ -1886,7 +1886,7 @@
"UP INTEG"} globally.
*}
-interpretation INTEG!: UP_pre_univ_prop INTEG INTEG id "UP INTEG"
+interpretation INTEG: UP_pre_univ_prop INTEG INTEG id "UP INTEG"
using INTEG_id_eval by simp_all
lemma INTEG_closed [intro, simp]:
--- a/src/HOL/Complex.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Complex.thy Thu Mar 26 20:08:55 2009 +0100
@@ -348,13 +348,13 @@
subsection {* Completeness of the Complexes *}
-interpretation Re!: bounded_linear "Re"
+interpretation Re: bounded_linear "Re"
apply (unfold_locales, simp, simp)
apply (rule_tac x=1 in exI)
apply (simp add: complex_norm_def)
done
-interpretation Im!: bounded_linear "Im"
+interpretation Im: bounded_linear "Im"
apply (unfold_locales, simp, simp)
apply (rule_tac x=1 in exI)
apply (simp add: complex_norm_def)
@@ -516,7 +516,7 @@
lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<twosuperior>"
by (simp add: norm_mult power2_eq_square)
-interpretation cnj!: bounded_linear "cnj"
+interpretation cnj: bounded_linear "cnj"
apply (unfold_locales)
apply (rule complex_cnj_add)
apply (rule complex_cnj_scaleR)
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Thu Mar 26 20:08:55 2009 +0100
@@ -637,7 +637,7 @@
using eq_diff_eq[where a= x and b=t and c=0] by simp
-interpretation class_ordered_field_dense_linear_order!: constr_dense_linear_order
+interpretation class_ordered_field_dense_linear_order: constr_dense_linear_order
"op <=" "op <"
"\<lambda> x y. 1/2 * ((x::'a::{ordered_field,recpower,number_ring}) + y)"
proof (unfold_locales, dlo, dlo, auto)
--- a/src/HOL/Divides.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Divides.thy Thu Mar 26 20:08:55 2009 +0100
@@ -852,7 +852,7 @@
text {* @{term "op dvd"} is a partial order *}
-interpretation dvd!: order "op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"
+interpretation dvd: order "op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"
proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym)
lemma nat_dvd_diff[simp]: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
--- a/src/HOL/Finite_Set.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Finite_Set.thy Thu Mar 26 20:08:55 2009 +0100
@@ -928,7 +928,7 @@
subsection {* Generalized summation over a set *}
-interpretation comm_monoid_add!: comm_monoid_mult "0::'a::comm_monoid_add" "op +"
+interpretation comm_monoid_add: comm_monoid_mult "0::'a::comm_monoid_add" "op +"
proof qed (auto intro: add_assoc add_commute)
definition setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
--- a/src/HOL/Groebner_Basis.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Groebner_Basis.thy Thu Mar 26 20:08:55 2009 +0100
@@ -163,7 +163,7 @@
end
-interpretation class_semiring!: gb_semiring
+interpretation class_semiring: gb_semiring
"op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"
proof qed (auto simp add: algebra_simps power_Suc)
@@ -242,7 +242,7 @@
end
-interpretation class_ring!: gb_ring "op +" "op *" "op ^"
+interpretation class_ring: gb_ring "op +" "op *" "op ^"
"0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"
proof qed simp_all
@@ -343,7 +343,7 @@
thus "b = 0" by blast
qed
-interpretation class_ringb!: ringb
+interpretation class_ringb: ringb
"op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"
proof(unfold_locales, simp add: algebra_simps power_Suc, auto)
fix w x y z ::"'a::{idom,recpower,number_ring}"
@@ -359,7 +359,7 @@
declaration {* normalizer_funs @{thm class_ringb.ringb_axioms'} *}
-interpretation natgb!: semiringb
+interpretation natgb: semiringb
"op +" "op *" "op ^" "0::nat" "1"
proof (unfold_locales, simp add: algebra_simps power_Suc)
fix w x y z ::"nat"
@@ -463,7 +463,7 @@
subsection{* Groebner Bases for fields *}
-interpretation class_fieldgb!:
+interpretation class_fieldgb:
fieldgb "op +" "op *" "op ^" "0::'a::{field,recpower,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse)
lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp
--- a/src/HOL/HahnBanach/Subspace.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/HahnBanach/Subspace.thy Thu Mar 26 20:08:55 2009 +0100
@@ -59,7 +59,7 @@
assumes "vectorspace V"
shows "0 \<in> U"
proof -
- interpret V!: vectorspace V by fact
+ interpret V: vectorspace V by fact
have "U \<noteq> {}" by (rule non_empty)
then obtain x where x: "x \<in> U" by blast
then have "x \<in> V" .. then have "0 = x - x" by simp
--- a/src/HOL/Lattices.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Lattices.thy Thu Mar 26 20:08:55 2009 +0100
@@ -299,7 +299,7 @@
by auto
qed (auto simp add: min_def max_def not_le less_imp_le)
-interpretation min_max!: distrib_lattice "op \<le> :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max
+interpretation min_max: distrib_lattice "op \<le> :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max
by (rule distrib_lattice_min_max)
lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{lower_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
--- a/src/HOL/Library/FrechetDeriv.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Library/FrechetDeriv.thy Thu Mar 26 20:08:55 2009 +0100
@@ -222,8 +222,8 @@
let ?k = "\<lambda>h. f (x + h) - f x"
let ?Nf = "\<lambda>h. norm (?Rf h) / norm h"
let ?Ng = "\<lambda>h. norm (?Rg (?k h)) / norm (?k h)"
- from f interpret F!: bounded_linear "F" by (rule FDERIV_bounded_linear)
- from g interpret G!: bounded_linear "G" by (rule FDERIV_bounded_linear)
+ from f interpret F: bounded_linear "F" by (rule FDERIV_bounded_linear)
+ from g interpret G: bounded_linear "G" by (rule FDERIV_bounded_linear)
from F.bounded obtain kF where kF: "\<And>x. norm (F x) \<le> norm x * kF" by fast
from G.bounded obtain kG where kG: "\<And>x. norm (G x) \<le> norm x * kG" by fast
--- a/src/HOL/Library/Inner_Product.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Library/Inner_Product.thy Thu Mar 26 20:08:55 2009 +0100
@@ -116,7 +116,7 @@
end
-interpretation inner!:
+interpretation inner:
bounded_bilinear "inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real"
proof
fix x y z :: 'a and r :: real
@@ -135,11 +135,11 @@
qed
qed
-interpretation inner_left!:
+interpretation inner_left:
bounded_linear "\<lambda>x::'a::real_inner. inner x y"
by (rule inner.bounded_linear_left)
-interpretation inner_right!:
+interpretation inner_right:
bounded_linear "\<lambda>y::'a::real_inner. inner x y"
by (rule inner.bounded_linear_right)
--- a/src/HOL/Library/Multiset.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Library/Multiset.thy Thu Mar 26 20:08:55 2009 +0100
@@ -1077,15 +1077,15 @@
apply simp
done
-interpretation mset_order!: order "op \<le>#" "op <#"
+interpretation mset_order: order "op \<le>#" "op <#"
proof qed (auto intro: order.intro mset_le_refl mset_le_antisym
mset_le_trans simp: mset_less_def)
-interpretation mset_order_cancel_semigroup!:
+interpretation mset_order_cancel_semigroup:
pordered_cancel_ab_semigroup_add "op +" "op \<le>#" "op <#"
proof qed (erule mset_le_mono_add [OF mset_le_refl])
-interpretation mset_order_semigroup_cancel!:
+interpretation mset_order_semigroup_cancel:
pordered_ab_semigroup_add_imp_le "op +" "op \<le>#" "op <#"
proof qed simp
@@ -1433,7 +1433,7 @@
definition [code del]:
"image_mset f = fold_mset (op + o single o f) {#}"
-interpretation image_left_comm!: left_commutative "op + o single o f"
+interpretation image_left_comm: left_commutative "op + o single o f"
proof qed (simp add:union_ac)
lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
--- a/src/HOL/Library/Numeral_Type.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Library/Numeral_Type.thy Thu Mar 26 20:08:55 2009 +0100
@@ -313,7 +313,7 @@
end
-interpretation bit0!:
+interpretation bit0:
mod_type "int CARD('a::finite bit0)"
"Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
"Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
@@ -329,7 +329,7 @@
apply (rule power_bit0_def [unfolded Abs_bit0'_def])
done
-interpretation bit1!:
+interpretation bit1:
mod_type "int CARD('a::finite bit1)"
"Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
"Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
@@ -363,13 +363,13 @@
end
-interpretation bit0!:
+interpretation bit0:
mod_ring "int CARD('a::finite bit0)"
"Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
"Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
..
-interpretation bit1!:
+interpretation bit1:
mod_ring "int CARD('a::finite bit1)"
"Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
"Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
--- a/src/HOL/Library/Product_Vector.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Library/Product_Vector.thy Thu Mar 26 20:08:55 2009 +0100
@@ -116,14 +116,14 @@
subsection {* Pair operations are linear and continuous *}
-interpretation fst!: bounded_linear fst
+interpretation fst: bounded_linear fst
apply (unfold_locales)
apply (rule fst_add)
apply (rule fst_scaleR)
apply (rule_tac x="1" in exI, simp add: norm_Pair)
done
-interpretation snd!: bounded_linear snd
+interpretation snd: bounded_linear snd
apply (unfold_locales)
apply (rule snd_add)
apply (rule snd_scaleR)
--- a/src/HOL/Library/SetsAndFunctions.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Library/SetsAndFunctions.thy Thu Mar 26 20:08:55 2009 +0100
@@ -107,26 +107,26 @@
apply simp
done
-interpretation set_semigroup_add!: semigroup_add "op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"
+interpretation set_semigroup_add: semigroup_add "op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"
apply default
apply (unfold set_plus_def)
apply (force simp add: add_assoc)
done
-interpretation set_semigroup_mult!: semigroup_mult "op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"
+interpretation set_semigroup_mult: semigroup_mult "op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"
apply default
apply (unfold set_times_def)
apply (force simp add: mult_assoc)
done
-interpretation set_comm_monoid_add!: comm_monoid_add "{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"
+interpretation set_comm_monoid_add: comm_monoid_add "{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"
apply default
apply (unfold set_plus_def)
apply (force simp add: add_ac)
apply force
done
-interpretation set_comm_monoid_mult!: comm_monoid_mult "{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"
+interpretation set_comm_monoid_mult: comm_monoid_mult "{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"
apply default
apply (unfold set_times_def)
apply (force simp add: mult_ac)
--- a/src/HOL/NSA/StarDef.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/NSA/StarDef.thy Thu Mar 26 20:08:55 2009 +0100
@@ -23,7 +23,7 @@
apply (rule nat_infinite)
done
-interpretation FreeUltrafilterNat!: freeultrafilter FreeUltrafilterNat
+interpretation FreeUltrafilterNat: freeultrafilter FreeUltrafilterNat
by (rule freeultrafilter_FreeUltrafilterNat)
text {* This rule takes the place of the old ultra tactic *}
--- a/src/HOL/RealVector.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/RealVector.thy Thu Mar 26 20:08:55 2009 +0100
@@ -145,7 +145,7 @@
and scaleR_scaleR: "scaleR a (scaleR b x) = scaleR (a * b) x"
and scaleR_one: "scaleR 1 x = x"
-interpretation real_vector!:
+interpretation real_vector:
vector_space "scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"
apply unfold_locales
apply (rule scaleR_right_distrib)
@@ -190,10 +190,10 @@
end
-interpretation scaleR_left!: additive "(\<lambda>a. scaleR a x::'a::real_vector)"
+interpretation scaleR_left: additive "(\<lambda>a. scaleR a x::'a::real_vector)"
proof qed (rule scaleR_left_distrib)
-interpretation scaleR_right!: additive "(\<lambda>x. scaleR a x::'a::real_vector)"
+interpretation scaleR_right: additive "(\<lambda>x. scaleR a x::'a::real_vector)"
proof qed (rule scaleR_right_distrib)
lemma nonzero_inverse_scaleR_distrib:
@@ -789,7 +789,7 @@
end
-interpretation mult!:
+interpretation mult:
bounded_bilinear "op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"
apply (rule bounded_bilinear.intro)
apply (rule left_distrib)
@@ -800,19 +800,19 @@
apply (simp add: norm_mult_ineq)
done
-interpretation mult_left!:
+interpretation mult_left:
bounded_linear "(\<lambda>x::'a::real_normed_algebra. x * y)"
by (rule mult.bounded_linear_left)
-interpretation mult_right!:
+interpretation mult_right:
bounded_linear "(\<lambda>y::'a::real_normed_algebra. x * y)"
by (rule mult.bounded_linear_right)
-interpretation divide!:
+interpretation divide:
bounded_linear "(\<lambda>x::'a::real_normed_field. x / y)"
unfolding divide_inverse by (rule mult.bounded_linear_left)
-interpretation scaleR!: bounded_bilinear "scaleR"
+interpretation scaleR: bounded_bilinear "scaleR"
apply (rule bounded_bilinear.intro)
apply (rule scaleR_left_distrib)
apply (rule scaleR_right_distrib)
@@ -822,13 +822,13 @@
apply (simp add: norm_scaleR)
done
-interpretation scaleR_left!: bounded_linear "\<lambda>r. scaleR r x"
+interpretation scaleR_left: bounded_linear "\<lambda>r. scaleR r x"
by (rule scaleR.bounded_linear_left)
-interpretation scaleR_right!: bounded_linear "\<lambda>x. scaleR r x"
+interpretation scaleR_right: bounded_linear "\<lambda>x. scaleR r x"
by (rule scaleR.bounded_linear_right)
-interpretation of_real!: bounded_linear "\<lambda>r. of_real r"
+interpretation of_real: bounded_linear "\<lambda>r. of_real r"
unfolding of_real_def by (rule scaleR.bounded_linear_left)
end
--- a/src/HOL/Word/TdThs.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Word/TdThs.thy Thu Mar 26 20:08:55 2009 +0100
@@ -89,7 +89,7 @@
end
-interpretation nat_int!: type_definition int nat "Collect (op <= 0)"
+interpretation nat_int: type_definition int nat "Collect (op <= 0)"
by (rule td_nat_int)
declare
--- a/src/HOL/Word/WordArith.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Word/WordArith.thy Thu Mar 26 20:08:55 2009 +0100
@@ -21,7 +21,7 @@
proof
qed (unfold word_sle_def word_sless_def, auto)
-interpretation signed!: linorder "word_sle" "word_sless"
+interpretation signed: linorder "word_sle" "word_sless"
by (rule signed_linorder)
lemmas word_arith_wis =
@@ -862,7 +862,7 @@
lemmas td_ext_unat = refl [THEN td_ext_unat']
lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm, standard]
-interpretation word_unat!:
+interpretation word_unat:
td_ext "unat::'a::len word => nat"
of_nat
"unats (len_of TYPE('a::len))"
--- a/src/HOL/Word/WordBitwise.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Word/WordBitwise.thy Thu Mar 26 20:08:55 2009 +0100
@@ -343,7 +343,7 @@
lemmas td_ext_nth = td_ext_nth' [OF refl refl refl, unfolded word_size]
-interpretation test_bit!:
+interpretation test_bit:
td_ext "op !! :: 'a::len0 word => nat => bool"
set_bits
"{f. \<forall>i. f i \<longrightarrow> i < len_of TYPE('a::len0)}"
--- a/src/HOL/Word/WordDefinition.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Word/WordDefinition.thy Thu Mar 26 20:08:55 2009 +0100
@@ -351,7 +351,7 @@
lemmas int_word_uint = td_ext_uint [THEN td_ext.eq_norm, standard]
-interpretation word_uint!:
+interpretation word_uint:
td_ext "uint::'a::len0 word \<Rightarrow> int"
word_of_int
"uints (len_of TYPE('a::len0))"
@@ -363,7 +363,7 @@
lemmas td_ext_ubin = td_ext_uint
[simplified len_gt_0 no_bintr_alt1 [symmetric]]
-interpretation word_ubin!:
+interpretation word_ubin:
td_ext "uint::'a::len0 word \<Rightarrow> int"
word_of_int
"uints (len_of TYPE('a::len0))"
@@ -418,7 +418,7 @@
and interpretations do not produce thm duplicates. I.e.
we get the name word_sint.Rep_eqD, but not word_sbin.Req_eqD,
because the latter is the same thm as the former *)
-interpretation word_sint!:
+interpretation word_sint:
td_ext "sint ::'a::len word => int"
word_of_int
"sints (len_of TYPE('a::len))"
@@ -426,7 +426,7 @@
2 ^ (len_of TYPE('a::len) - 1)"
by (rule td_ext_sint)
-interpretation word_sbin!:
+interpretation word_sbin:
td_ext "sint ::'a::len word => int"
word_of_int
"sints (len_of TYPE('a::len))"
@@ -630,7 +630,7 @@
apply simp
done
-interpretation word_bl!:
+interpretation word_bl:
type_definition "to_bl :: 'a::len0 word => bool list"
of_bl
"{bl. length bl = len_of TYPE('a::len0)}"
--- a/src/HOL/Word/WordGenLib.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Word/WordGenLib.thy Thu Mar 26 20:08:55 2009 +0100
@@ -106,7 +106,7 @@
apply (rule word_or_not)
done
-interpretation word_bool_alg!:
+interpretation word_bool_alg:
boolean "op AND" "op OR" bitNOT 0 max_word
by (rule word_boolean)
@@ -114,7 +114,7 @@
"x XOR y = x AND NOT y OR NOT x AND (y::'a::len0 word)"
by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
-interpretation word_bool_alg!:
+interpretation word_bool_alg:
boolean_xor "op AND" "op OR" bitNOT 0 max_word "op XOR"
apply (rule boolean_xor.intro)
apply (rule word_boolean)
--- a/src/HOL/ex/LocaleTest2.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/ex/LocaleTest2.thy Thu Mar 26 20:08:55 2009 +0100
@@ -468,7 +468,7 @@
subsubsection {* Total order @{text "<="} on @{typ int} *}
-interpretation int!: dpo "op <= :: [int, int] => bool"
+interpretation int: dpo "op <= :: [int, int] => bool"
where "(dpo.less (op <=) (x::int) y) = (x < y)"
txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
proof -
@@ -487,7 +487,7 @@
lemma "(op < :: [int, int] => bool) = op <"
apply (rule int.abs_test) done
-interpretation int!: dlat "op <= :: [int, int] => bool"
+interpretation int: dlat "op <= :: [int, int] => bool"
where meet_eq: "dlat.meet (op <=) (x::int) y = min x y"
and join_eq: "dlat.join (op <=) (x::int) y = max x y"
proof -
@@ -511,7 +511,7 @@
by auto
qed
-interpretation int!: dlo "op <= :: [int, int] => bool"
+interpretation int: dlo "op <= :: [int, int] => bool"
proof qed arith
text {* Interpreted theorems from the locales, involving defined terms. *}
@@ -524,7 +524,7 @@
subsubsection {* Total order @{text "<="} on @{typ nat} *}
-interpretation nat!: dpo "op <= :: [nat, nat] => bool"
+interpretation nat: dpo "op <= :: [nat, nat] => bool"
where "dpo.less (op <=) (x::nat) y = (x < y)"
txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
proof -
@@ -538,7 +538,7 @@
done
qed
-interpretation nat!: dlat "op <= :: [nat, nat] => bool"
+interpretation nat: dlat "op <= :: [nat, nat] => bool"
where "dlat.meet (op <=) (x::nat) y = min x y"
and "dlat.join (op <=) (x::nat) y = max x y"
proof -
@@ -562,7 +562,7 @@
by auto
qed
-interpretation nat!: dlo "op <= :: [nat, nat] => bool"
+interpretation nat: dlo "op <= :: [nat, nat] => bool"
proof qed arith
text {* Interpreted theorems from the locales, involving defined terms. *}
@@ -575,7 +575,7 @@
subsubsection {* Lattice @{text "dvd"} on @{typ nat} *}
-interpretation nat_dvd!: dpo "op dvd :: [nat, nat] => bool"
+interpretation nat_dvd: dpo "op dvd :: [nat, nat] => bool"
where "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
proof -
@@ -589,7 +589,7 @@
done
qed
-interpretation nat_dvd!: dlat "op dvd :: [nat, nat] => bool"
+interpretation nat_dvd: dlat "op dvd :: [nat, nat] => bool"
where "dlat.meet (op dvd) (x::nat) y = gcd x y"
and "dlat.join (op dvd) (x::nat) y = lcm x y"
proof -
@@ -834,7 +834,7 @@
subsubsection {* Interpretation of Functions *}
-interpretation Dfun!: Dmonoid "op o" "id :: 'a => 'a"
+interpretation Dfun: Dmonoid "op o" "id :: 'a => 'a"
where "Dmonoid.unit (op o) id f = bij (f::'a => 'a)"
(* and "Dmonoid.inv (op o) id" = "inv :: ('a => 'a) => ('a => 'a)" *)
proof -
@@ -884,7 +884,7 @@
"(f :: unit => unit) = id"
by rule simp
-interpretation Dfun!: Dgrp "op o" "id :: unit => unit"
+interpretation Dfun: Dgrp "op o" "id :: unit => unit"
where "Dmonoid.inv (op o) id f = inv (f :: unit => unit)"
proof -
have "Dmonoid op o (id :: 'a => 'a)" ..
--- a/src/HOLCF/Algebraic.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOLCF/Algebraic.thy Thu Mar 26 20:08:55 2009 +0100
@@ -215,7 +215,7 @@
lemma finite_deflation_Rep_fin_defl: "finite_deflation (Rep_fin_defl d)"
using Rep_fin_defl by simp
-interpretation Rep_fin_defl!: finite_deflation "Rep_fin_defl d"
+interpretation Rep_fin_defl: finite_deflation "Rep_fin_defl d"
by (rule finite_deflation_Rep_fin_defl)
lemma fin_defl_lessI:
@@ -320,7 +320,7 @@
apply (rule Rep_fin_defl.compact)
done
-interpretation fin_defl!: basis_take sq_le fd_take
+interpretation fin_defl: basis_take sq_le fd_take
apply default
apply (rule fd_take_less)
apply (rule fd_take_idem)
@@ -370,7 +370,7 @@
unfolding alg_defl_principal_def
by (simp add: Abs_alg_defl_inverse sq_le.ideal_principal)
-interpretation alg_defl!:
+interpretation alg_defl:
ideal_completion sq_le fd_take alg_defl_principal Rep_alg_defl
apply default
apply (rule ideal_Rep_alg_defl)
@@ -461,7 +461,7 @@
apply (rule finite_deflation_Rep_fin_defl)
done
-interpretation cast!: deflation "cast\<cdot>d"
+interpretation cast: deflation "cast\<cdot>d"
by (rule deflation_cast)
lemma "cast\<cdot>(\<Squnion>i. alg_defl_principal (Abs_fin_defl (approx i)))\<cdot>x = x"
--- a/src/HOLCF/Bifinite.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOLCF/Bifinite.thy Thu Mar 26 20:08:55 2009 +0100
@@ -37,7 +37,7 @@
by (rule finite_fixes_approx)
qed
-interpretation approx!: finite_deflation "approx i"
+interpretation approx: finite_deflation "approx i"
by (rule finite_deflation_approx)
lemma (in deflation) deflation: "deflation d" ..
--- a/src/HOLCF/CompactBasis.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOLCF/CompactBasis.thy Thu Mar 26 20:08:55 2009 +0100
@@ -46,7 +46,7 @@
lemmas approx_Rep_compact_basis = Rep_compact_take [symmetric]
-interpretation compact_basis!:
+interpretation compact_basis:
basis_take sq_le compact_take
proof
fix n :: nat and a :: "'a compact_basis"
@@ -92,7 +92,7 @@
approximants :: "'a \<Rightarrow> 'a compact_basis set" where
"approximants = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
-interpretation compact_basis!:
+interpretation compact_basis:
ideal_completion sq_le compact_take Rep_compact_basis approximants
proof
fix w :: 'a
--- a/src/HOLCF/Completion.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOLCF/Completion.thy Thu Mar 26 20:08:55 2009 +0100
@@ -156,7 +156,7 @@
end
-interpretation sq_le!: preorder "sq_le :: 'a::po \<Rightarrow> 'a \<Rightarrow> bool"
+interpretation sq_le: preorder "sq_le :: 'a::po \<Rightarrow> 'a \<Rightarrow> bool"
apply unfold_locales
apply (rule refl_less)
apply (erule (1) trans_less)
--- a/src/HOLCF/ConvexPD.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOLCF/ConvexPD.thy Thu Mar 26 20:08:55 2009 +0100
@@ -20,7 +20,7 @@
lemma convex_le_trans: "\<lbrakk>t \<le>\<natural> u; u \<le>\<natural> v\<rbrakk> \<Longrightarrow> t \<le>\<natural> v"
unfolding convex_le_def by (fast intro: upper_le_trans lower_le_trans)
-interpretation convex_le!: preorder convex_le
+interpretation convex_le: preorder convex_le
by (rule preorder.intro, rule convex_le_refl, rule convex_le_trans)
lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<natural> t"
@@ -178,7 +178,7 @@
unfolding convex_principal_def
by (simp add: Abs_convex_pd_inverse convex_le.ideal_principal)
-interpretation convex_pd!:
+interpretation convex_pd:
ideal_completion convex_le pd_take convex_principal Rep_convex_pd
apply unfold_locales
apply (rule pd_take_convex_le)
--- a/src/HOLCF/LowerPD.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOLCF/LowerPD.thy Thu Mar 26 20:08:55 2009 +0100
@@ -26,7 +26,7 @@
apply (erule (1) trans_less)
done
-interpretation lower_le!: preorder lower_le
+interpretation lower_le: preorder lower_le
by (rule preorder.intro, rule lower_le_refl, rule lower_le_trans)
lemma lower_le_minimal [simp]: "PDUnit compact_bot \<le>\<flat> t"
@@ -133,7 +133,7 @@
unfolding lower_principal_def
by (simp add: Abs_lower_pd_inverse lower_le.ideal_principal)
-interpretation lower_pd!:
+interpretation lower_pd:
ideal_completion lower_le pd_take lower_principal Rep_lower_pd
apply unfold_locales
apply (rule pd_take_lower_le)
--- a/src/HOLCF/Universal.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOLCF/Universal.thy Thu Mar 26 20:08:55 2009 +0100
@@ -230,13 +230,13 @@
apply (simp add: ubasis_take_same)
done
-interpretation udom!: preorder ubasis_le
+interpretation udom: preorder ubasis_le
apply default
apply (rule ubasis_le_refl)
apply (erule (1) ubasis_le_trans)
done
-interpretation udom!: basis_take ubasis_le ubasis_take
+interpretation udom: basis_take ubasis_le ubasis_take
apply default
apply (rule ubasis_take_less)
apply (rule ubasis_take_idem)
@@ -285,7 +285,7 @@
unfolding udom_principal_def
by (simp add: Abs_udom_inverse udom.ideal_principal)
-interpretation udom!:
+interpretation udom:
ideal_completion ubasis_le ubasis_take udom_principal Rep_udom
apply unfold_locales
apply (rule ideal_Rep_udom)
--- a/src/HOLCF/UpperPD.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOLCF/UpperPD.thy Thu Mar 26 20:08:55 2009 +0100
@@ -26,7 +26,7 @@
apply (erule (1) trans_less)
done
-interpretation upper_le!: preorder upper_le
+interpretation upper_le: preorder upper_le
by (rule preorder.intro, rule upper_le_refl, rule upper_le_trans)
lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<sharp> t"
@@ -131,7 +131,7 @@
unfolding upper_principal_def
by (simp add: Abs_upper_pd_inverse upper_le.ideal_principal)
-interpretation upper_pd!:
+interpretation upper_pd:
ideal_completion upper_le pd_take upper_principal Rep_upper_pd
apply unfold_locales
apply (rule pd_take_upper_le)
--- a/src/ZF/Constructible/L_axioms.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/ZF/Constructible/L_axioms.thy Thu Mar 26 20:08:55 2009 +0100
@@ -99,7 +99,7 @@
apply (rule L_nat)
done
-interpretation L: M_trivial L by (rule M_trivial_L)
+interpretation L?: M_trivial L by (rule M_trivial_L)
(* Replaces the following declarations...
lemmas rall_abs = M_trivial.rall_abs [OF M_trivial_L]
--- a/src/ZF/Constructible/Rec_Separation.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/ZF/Constructible/Rec_Separation.thy Thu Mar 26 20:08:55 2009 +0100
@@ -185,7 +185,7 @@
theorem M_trancl_L: "PROP M_trancl(L)"
by (rule M_trancl.intro [OF M_basic_L M_trancl_axioms_L])
-interpretation L: M_trancl L by (rule M_trancl_L)
+interpretation L?: M_trancl L by (rule M_trancl_L)
subsection{*@{term L} is Closed Under the Operator @{term list}*}
@@ -372,7 +372,7 @@
apply (rule M_datatypes_axioms_L)
done
-interpretation L: M_datatypes L by (rule M_datatypes_L)
+interpretation L?: M_datatypes L by (rule M_datatypes_L)
subsection{*@{term L} is Closed Under the Operator @{term eclose}*}
@@ -435,7 +435,7 @@
apply (rule M_eclose_axioms_L)
done
-interpretation L: M_eclose L by (rule M_eclose_L)
+interpretation L?: M_eclose L by (rule M_eclose_L)
end
--- a/src/ZF/Constructible/Separation.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/ZF/Constructible/Separation.thy Thu Mar 26 20:08:55 2009 +0100
@@ -305,7 +305,7 @@
theorem M_basic_L: "PROP M_basic(L)"
by (rule M_basic.intro [OF M_trivial_L M_basic_axioms_L])
-interpretation L: M_basic L by (rule M_basic_L)
+interpretation L?: M_basic L by (rule M_basic_L)
end