# HG changeset patch # User wenzelm # Date 1238094535 -3600 # Node ID 461ee3e49ad3bf8518f0d051f89dc6faf4361d04 # Parent f0aeca99b5d937192811f6c17a7eedd85c23edba interpretation/interpret: prefixes are mandatory by default; diff -r f0aeca99b5d9 -r 461ee3e49ad3 doc-src/Classes/Thy/Classes.thy --- 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 "[]" .. diff -r f0aeca99b5d9 -r 461ee3e49ad3 doc-src/Classes/Thy/document/Classes.tex --- 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)\\ diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/FOL/ex/LocaleTest.thy --- 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+ diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/Algebra/AbelCoset.thy --- 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 \ carrier G" "x' \ carrier G" shows "(x' \ H +> x) = (x' \ x \ H)" proof - - interpret G!: ring G by fact + interpret G: ring G by fact from carr have "(x' \ H +> x) = (x' \ \x \ H)" by (rule a_rcos_module) with carr diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/Algebra/Group.thy --- 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 \\ 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 \\ 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 \ carrier H" shows "m_inv (G \\ 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 \\ H" + interpret G: group G by fact + interpret H: group H by fact + interpret Prod: group "G \\ H" by (auto intro: DirProd_group group.intro group.axioms assms) show ?thesis by (simp add: Prod.inv_equality g h) qed diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/Algebra/Ideal.thy --- 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" | "\a b. a \ carrier R \ b \ carrier R \ a \ b \ I \ a \ I \ b \ I" proof - - interpret R!: cring R by fact + interpret R: cring R by fact assume "carrier R = I ==> thesis" and "\a b. a \ carrier R \ b \ carrier R \ a \ b \ I \ a \ I \ b \ I \ thesis" then show thesis using primeidealCD [OF R.is_cring notprime] by blast diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/Algebra/IntRing.thy --- 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 \ +interpretation int: monoid \ where "carrier \ = UNIV" and "mult \ x y = x * y" and "one \ = 1" @@ -104,7 +104,7 @@ proof - -- "Specification" show "monoid \" proof qed (auto simp: int_ring_def) - then interpret int!: monoid \ . + then interpret int: monoid \ . -- "Carrier" show "carrier \ = UNIV" by (simp add: int_ring_def) @@ -116,12 +116,12 @@ show "pow \ x n = x^n" by (induct n) (simp, simp add: int_ring_def)+ qed -interpretation int!: comm_monoid \ +interpretation int: comm_monoid \ where "finprod \ f A = (if finite A then setprod f A else undefined)" proof - -- "Specification" show "comm_monoid \" proof qed (auto simp: int_ring_def) - then interpret int!: comm_monoid \ . + then interpret int: comm_monoid \ . -- "Operations" { fix x y have "mult \ x y = x * y" by (simp add: int_ring_def) } @@ -139,14 +139,14 @@ qed qed -interpretation int!: abelian_monoid \ +interpretation int: abelian_monoid \ where "zero \ = 0" and "add \ x y = x + y" and "finsum \ f A = (if finite A then setsum f A else undefined)" proof - -- "Specification" show "abelian_monoid \" proof qed (auto simp: int_ring_def) - then interpret int!: abelian_monoid \ . + then interpret int: abelian_monoid \ . -- "Operations" { fix x y show "add \ x y = x + y" by (simp add: int_ring_def) } @@ -164,7 +164,7 @@ qed qed -interpretation int!: abelian_group \ +interpretation int: abelian_group \ where "a_inv \ x = - x" and "a_minus \ x y = x - y" proof - @@ -174,7 +174,7 @@ show "!!x. x \ carrier \ ==> EX y : carrier \. y \\<^bsub>\\<^esub> x = \\<^bsub>\\<^esub>" by (simp add: int_ring_def) arith qed (auto simp: int_ring_def) - then interpret int!: abelian_group \ . + then interpret int: abelian_group \ . -- "Operations" { fix x y have "add \ x y = x + y" by (simp add: int_ring_def) } @@ -187,7 +187,7 @@ show "a_minus \ x y = x - y" by (simp add: int.minus_eq add a_inv) qed -interpretation int!: "domain" \ +interpretation int: "domain" \ 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 \ |)" where "carrier (| carrier = UNIV::int set, eq = op =, le = op \ |) = UNIV" and "le (| carrier = UNIV::int set, eq = op =, le = op \ |) x y = (x \ 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 \ |)" where "join (| carrier = UNIV::int set, eq = op =, le = op \ |) x y = max x y" and "meet (| carrier = UNIV::int set, eq = op =, le = op \ |) 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 \ |)" proof qed clarsimp diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/Algebra/RingHom.thy --- 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 \ 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 diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/Algebra/UnivPoly.thy --- 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]: diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/Complex.thy --- 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)\" 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) diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/Decision_Procs/Dense_Linear_Order.thy --- 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 <" "\ x y. 1/2 * ((x::'a::{ordered_field,recpower,number_ring}) + y)" proof (unfold_locales, dlo, dlo, auto) diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/Divides.thy --- 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" "\n m \ nat. n dvd m \ \ m dvd n" +interpretation dvd: order "op dvd" "\n m \ nat. n dvd m \ \ 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)" diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/Finite_Set.thy --- 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" diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/Groebner_Basis.thy --- 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 diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/HahnBanach/Subspace.thy --- 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 \ U" proof - - interpret V!: vectorspace V by fact + interpret V: vectorspace V by fact have "U \ {}" by (rule non_empty) then obtain x where x: "x \ U" by blast then have "x \ V" .. then have "0 = x - x" by simp diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/Lattices.thy --- 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 \ :: 'a::linorder \ 'a \ bool" "op <" min max +interpretation min_max: distrib_lattice "op \ :: 'a::linorder \ 'a \ bool" "op <" min max by (rule distrib_lattice_min_max) lemma inf_min: "inf = (min \ 'a\{lower_semilattice, linorder} \ 'a \ 'a)" diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/Library/FrechetDeriv.thy --- 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 = "\h. f (x + h) - f x" let ?Nf = "\h. norm (?Rf h) / norm h" let ?Ng = "\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: "\x. norm (F x) \ norm x * kF" by fast from G.bounded obtain kG where kG: "\x. norm (G x) \ norm x * kG" by fast diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/Library/Inner_Product.thy --- 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 \ 'a \ real" proof fix x y z :: 'a and r :: real @@ -135,11 +135,11 @@ qed qed -interpretation inner_left!: +interpretation inner_left: bounded_linear "\x::'a::real_inner. inner x y" by (rule inner.bounded_linear_left) -interpretation inner_right!: +interpretation inner_right: bounded_linear "\y::'a::real_inner. inner x y" by (rule inner.bounded_linear_right) diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/Library/Multiset.thy --- 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 \#" "op <#" +interpretation mset_order: order "op \#" "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 \#" "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 \#" "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 {#} = {#}" diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/Library/Numeral_Type.thy --- 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 \ int" "Abs_bit0 :: int \ '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 \ int" "Abs_bit1 :: int \ 'a::finite bit1" @@ -363,13 +363,13 @@ end -interpretation bit0!: +interpretation bit0: mod_ring "int CARD('a::finite bit0)" "Rep_bit0 :: 'a::finite bit0 \ int" "Abs_bit0 :: int \ 'a::finite bit0" .. -interpretation bit1!: +interpretation bit1: mod_ring "int CARD('a::finite bit1)" "Rep_bit1 :: 'a::finite bit1 \ int" "Abs_bit1 :: int \ 'a::finite bit1" diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/Library/Product_Vector.thy --- 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) diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/Library/SetsAndFunctions.thy --- 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 \ :: ('a::semigroup_add) set => 'a set => 'a set" +interpretation set_semigroup_add: semigroup_add "op \ :: ('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 \ :: ('a::semigroup_mult) set => 'a set => 'a set" +interpretation set_semigroup_mult: semigroup_mult "op \ :: ('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 \ :: ('a::comm_monoid_add) set => 'a set => 'a set" +interpretation set_comm_monoid_add: comm_monoid_add "{0}" "op \ :: ('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 \ :: ('a::comm_monoid_mult) set => 'a set => 'a set" +interpretation set_comm_monoid_mult: comm_monoid_mult "{1}" "op \ :: ('a::comm_monoid_mult) set => 'a set => 'a set" apply default apply (unfold set_times_def) apply (force simp add: mult_ac) diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/NSA/StarDef.thy --- 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 *} diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/RealVector.thy --- 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 \ 'a \ 'a::real_vector" apply unfold_locales apply (rule scaleR_right_distrib) @@ -190,10 +190,10 @@ end -interpretation scaleR_left!: additive "(\a. scaleR a x::'a::real_vector)" +interpretation scaleR_left: additive "(\a. scaleR a x::'a::real_vector)" proof qed (rule scaleR_left_distrib) -interpretation scaleR_right!: additive "(\x. scaleR a x::'a::real_vector)" +interpretation scaleR_right: additive "(\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 \ 'a \ '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 "(\x::'a::real_normed_algebra. x * y)" by (rule mult.bounded_linear_left) -interpretation mult_right!: +interpretation mult_right: bounded_linear "(\y::'a::real_normed_algebra. x * y)" by (rule mult.bounded_linear_right) -interpretation divide!: +interpretation divide: bounded_linear "(\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 "\r. scaleR r x" +interpretation scaleR_left: bounded_linear "\r. scaleR r x" by (rule scaleR.bounded_linear_left) -interpretation scaleR_right!: bounded_linear "\x. scaleR r x" +interpretation scaleR_right: bounded_linear "\x. scaleR r x" by (rule scaleR.bounded_linear_right) -interpretation of_real!: bounded_linear "\r. of_real r" +interpretation of_real: bounded_linear "\r. of_real r" unfolding of_real_def by (rule scaleR.bounded_linear_left) end diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/Word/TdThs.thy --- 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 diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/Word/WordArith.thy --- 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))" diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/Word/WordBitwise.thy --- 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. \i. f i \ i < len_of TYPE('a::len0)}" diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/Word/WordDefinition.thy --- 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 \ 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 \ 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)}" diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/Word/WordGenLib.thy --- 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) diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/ex/LocaleTest2.thy --- 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)" .. diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOLCF/Algebraic.thy --- 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\d" +interpretation cast: deflation "cast\d" by (rule deflation_cast) lemma "cast\(\i. alg_defl_principal (Abs_fin_defl (approx i)))\x = x" diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOLCF/Bifinite.thy --- 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" .. diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOLCF/CompactBasis.thy --- 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 \ 'a compact_basis set" where "approximants = (\x. {a. Rep_compact_basis a \ x})" -interpretation compact_basis!: +interpretation compact_basis: ideal_completion sq_le compact_take Rep_compact_basis approximants proof fix w :: 'a diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOLCF/Completion.thy --- 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 \ 'a \ bool" +interpretation sq_le: preorder "sq_le :: 'a::po \ 'a \ bool" apply unfold_locales apply (rule refl_less) apply (erule (1) trans_less) diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOLCF/ConvexPD.thy --- 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: "\t \\ u; u \\ v\ \ t \\ 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 \\ 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) diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOLCF/LowerPD.thy --- 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 \\ 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) diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOLCF/Universal.thy --- 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) diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOLCF/UpperPD.thy --- 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 \\ 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) diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/ZF/Constructible/L_axioms.thy --- 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] diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/ZF/Constructible/Rec_Separation.thy --- 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 diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/ZF/Constructible/Separation.thy --- 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