1.1 --- a/doc-src/Classes/Thy/Classes.thy	Thu Mar 26 19:24:21 2009 +0100
     1.2 +++ b/doc-src/Classes/Thy/Classes.thy	Thu Mar 26 20:08:55 2009 +0100
     1.3 @@ -458,7 +458,7 @@
     1.4    of monoids for lists:
     1.5  *}
     1.6  
     1.7 -interpretation %quote list_monoid!: monoid append "[]"
     1.8 +interpretation %quote list_monoid: monoid append "[]"
     1.9    proof qed auto
    1.10  
    1.11  text {*
    1.12 @@ -473,7 +473,7 @@
    1.13    "replicate 0 _ = []"
    1.14    | "replicate (Suc n) xs = xs @ replicate n xs"
    1.15  
    1.16 -interpretation %quote list_monoid!: monoid append "[]" where
    1.17 +interpretation %quote list_monoid: monoid append "[]" where
    1.18    "monoid.pow_nat append [] = replicate"
    1.19  proof -
    1.20    interpret monoid append "[]" ..

     2.1 --- a/doc-src/Classes/Thy/document/Classes.tex	Thu Mar 26 19:24:21 2009 +0100
     2.2 +++ b/doc-src/Classes/Thy/document/Classes.tex	Thu Mar 26 20:08:55 2009 +0100
     2.3 @@ -863,7 +863,7 @@
     2.4  %
     2.5  \isatagquote
     2.6  \isacommand{interpretation}\isamarkupfalse%
     2.7 -\ list{\isacharunderscore}monoid{\isacharbang}{\isacharcolon}\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
     2.8 +\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
     2.9  \ \ \isacommand{proof}\isamarkupfalse%
    2.10  \ \isacommand{qed}\isamarkupfalse%
    2.11  \ auto%
    2.12 @@ -894,7 +894,7 @@
    2.13  \ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline
    2.14  \isanewline
    2.15  \isacommand{interpretation}\isamarkupfalse%
    2.16 -\ list{\isacharunderscore}monoid{\isacharbang}{\isacharcolon}\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
    2.17 +\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
    2.18  \ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
    2.19  \isacommand{proof}\isamarkupfalse%
    2.20  \ {\isacharminus}\isanewline
    2.21 @@ -1191,7 +1191,7 @@
    2.22  \hspace*{0pt}\\
    2.23  \hspace*{0pt}pow{\char95}nat ::~forall a.~(Monoid a) => Nat -> a -> a;\\
    2.24  \hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\
    2.25 -\hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\
    2.26 +\hspace*{0pt}pow{\char95}nat (Suc n) xa = mult xa (pow{\char95}nat n xa);\\
    2.27  \hspace*{0pt}\\
    2.28  \hspace*{0pt}pow{\char95}int ::~forall a.~(Group a) => Integer -> a -> a;\\
    2.29  \hspace*{0pt}pow{\char95}int k x =\\
    2.30 @@ -1272,8 +1272,8 @@
    2.31  \hspace*{0pt} ~IntInf.int group;\\
    2.32  \hspace*{0pt}\\
    2.33  \hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\
    2.34 -\hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) x =\\
    2.35 -\hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) x (pow{\char95}nat A{\char95}~n x);\\
    2.36 +\hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) xa =\\
    2.37 +\hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) xa (pow{\char95}nat A{\char95}~n xa);\\
    2.38  \hspace*{0pt}\\
    2.39  \hspace*{0pt}fun pow{\char95}int A{\char95}~k x =\\
    2.40  \hspace*{0pt} ~(if IntInf.<= ((0 :~IntInf.int),~k)\\

     3.1 --- a/src/FOL/ex/LocaleTest.thy	Thu Mar 26 19:24:21 2009 +0100
     3.2 +++ b/src/FOL/ex/LocaleTest.thy	Thu Mar 26 20:08:55 2009 +0100
     3.3 @@ -119,7 +119,7 @@
     3.4  
     3.5  term extra_type.test thm extra_type.test_def
     3.6  
     3.7 -interpretation var: extra_type "0" "%x y. x = 0" .
     3.8 +interpretation var?: extra_type "0" "%x y. x = 0" .
     3.9  
    3.10  thm var.test_def
    3.11  
    3.12 @@ -381,13 +381,13 @@
    3.13  
    3.14  subsection {* Sublocale, then interpretation in theory *}
    3.15  
    3.16 -interpretation int: lgrp "op +" "0" "minus"
    3.17 +interpretation int?: lgrp "op +" "0" "minus"
    3.18  proof unfold_locales
    3.19  qed (rule int_assoc int_zero int_minus)+
    3.20  
    3.21  thm int.assoc int.semi_axioms
    3.22  
    3.23 -interpretation int2: semi "op +"
    3.24 +interpretation int2?: semi "op +"
    3.25    by unfold_locales  (* subsumed, thm int2.assoc not generated *)
    3.26  
    3.27  thm int.lone int.right.rone
    3.28 @@ -443,7 +443,7 @@
    3.29  
    3.30  end
    3.31  
    3.32 -interpretation x!: logic_o "op &" "Not"
    3.33 +interpretation x: logic_o "op &" "Not"
    3.34    where bool_logic_o: "logic_o.lor_o(op &, Not, x, y) <-> x | y"
    3.35  proof -
    3.36    show bool_logic_o: "PROP logic_o(op &, Not)" by unfold_locales fast+

     4.1 --- a/src/HOL/Algebra/AbelCoset.thy	Thu Mar 26 19:24:21 2009 +0100
     4.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Thu Mar 26 20:08:55 2009 +0100
     4.3 @@ -540,8 +540,8 @@
     4.4                                    (| carrier = carrier H, mult = add H, one = zero H |) h"
     4.5    shows "abelian_group_hom G H h"
     4.6  proof -
     4.7 -  interpret G!: abelian_group G by fact
     4.8 -  interpret H!: abelian_group H by fact
     4.9 +  interpret G: abelian_group G by fact
    4.10 +  interpret H: abelian_group H by fact
    4.11    show ?thesis apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
    4.12      apply fact
    4.13      apply fact
    4.14 @@ -692,7 +692,7 @@
    4.15    assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
    4.16    shows "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
    4.17  proof -
    4.18 -  interpret G!: ring G by fact
    4.19 +  interpret G: ring G by fact
    4.20    from carr
    4.21    have "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)" by (rule a_rcos_module)
    4.22    with carr

     5.1 --- a/src/HOL/Algebra/Group.thy	Thu Mar 26 19:24:21 2009 +0100
     5.2 +++ b/src/HOL/Algebra/Group.thy	Thu Mar 26 20:08:55 2009 +0100
     5.3 @@ -488,8 +488,8 @@
     5.4    assumes "monoid G" and "monoid H"
     5.5    shows "monoid (G \<times>\<times> H)"
     5.6  proof -
     5.7 -  interpret G!: monoid G by fact
     5.8 -  interpret H!: monoid H by fact
     5.9 +  interpret G: monoid G by fact
    5.10 +  interpret H: monoid H by fact
    5.11    from assms
    5.12    show ?thesis by (unfold monoid_def DirProd_def, auto) 
    5.13  qed
    5.14 @@ -500,8 +500,8 @@
    5.15    assumes "group G" and "group H"
    5.16    shows "group (G \<times>\<times> H)"
    5.17  proof -
    5.18 -  interpret G!: group G by fact
    5.19 -  interpret H!: group H by fact
    5.20 +  interpret G: group G by fact
    5.21 +  interpret H: group H by fact
    5.22    show ?thesis by (rule groupI)
    5.23       (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
    5.24             simp add: DirProd_def)
    5.25 @@ -525,9 +525,9 @@
    5.26        and h: "h \<in> carrier H"
    5.27    shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
    5.28  proof -
    5.29 -  interpret G!: group G by fact
    5.30 -  interpret H!: group H by fact
    5.31 -  interpret Prod!: group "G \<times>\<times> H"
    5.32 +  interpret G: group G by fact
    5.33 +  interpret H: group H by fact
    5.34 +  interpret Prod: group "G \<times>\<times> H"
    5.35      by (auto intro: DirProd_group group.intro group.axioms assms)
    5.36    show ?thesis by (simp add: Prod.inv_equality g h)
    5.37  qed

     6.1 --- a/src/HOL/Algebra/Ideal.thy	Thu Mar 26 19:24:21 2009 +0100
     6.2 +++ b/src/HOL/Algebra/Ideal.thy	Thu Mar 26 20:08:55 2009 +0100
     6.3 @@ -711,7 +711,7 @@
     6.4    obtains "carrier R = I"
     6.5      | "\<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"
     6.6  proof -
     6.7 -  interpret R!: cring R by fact
     6.8 +  interpret R: cring R by fact
     6.9    assume "carrier R = I ==> thesis"
    6.10      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"
    6.11    then show thesis using primeidealCD [OF R.is_cring notprime] by blast

     7.1 --- a/src/HOL/Algebra/IntRing.thy	Thu Mar 26 19:24:21 2009 +0100
     7.2 +++ b/src/HOL/Algebra/IntRing.thy	Thu Mar 26 20:08:55 2009 +0100
     7.3 @@ -96,7 +96,7 @@
     7.4    interpretation needs to be done as early as possible --- that is,
     7.5    with as few assumptions as possible. *}
     7.6  
     7.7 -interpretation int!: monoid \<Z>
     7.8 +interpretation int: monoid \<Z>
     7.9    where "carrier \<Z> = UNIV"
    7.10      and "mult \<Z> x y = x * y"
    7.11      and "one \<Z> = 1"
    7.12 @@ -104,7 +104,7 @@
    7.13  proof -
    7.14    -- "Specification"
    7.15    show "monoid \<Z>" proof qed (auto simp: int_ring_def)
    7.16 -  then interpret int!: monoid \<Z> .
    7.17 +  then interpret int: monoid \<Z> .
    7.18  
    7.19    -- "Carrier"
    7.20    show "carrier \<Z> = UNIV" by (simp add: int_ring_def)
    7.21 @@ -116,12 +116,12 @@
    7.22    show "pow \<Z> x n = x^n" by (induct n) (simp, simp add: int_ring_def)+
    7.23  qed
    7.24  
    7.25 -interpretation int!: comm_monoid \<Z>
    7.26 +interpretation int: comm_monoid \<Z>
    7.27    where "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
    7.28  proof -
    7.29    -- "Specification"
    7.30    show "comm_monoid \<Z>" proof qed (auto simp: int_ring_def)
    7.31 -  then interpret int!: comm_monoid \<Z> .
    7.32 +  then interpret int: comm_monoid \<Z> .
    7.33  
    7.34    -- "Operations"
    7.35    { fix x y have "mult \<Z> x y = x * y" by (simp add: int_ring_def) }
    7.36 @@ -139,14 +139,14 @@
    7.37    qed
    7.38  qed
    7.39  
    7.40 -interpretation int!: abelian_monoid \<Z>
    7.41 +interpretation int: abelian_monoid \<Z>
    7.42    where "zero \<Z> = 0"
    7.43      and "add \<Z> x y = x + y"
    7.44      and "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
    7.45  proof -
    7.46    -- "Specification"
    7.47    show "abelian_monoid \<Z>" proof qed (auto simp: int_ring_def)
    7.48 -  then interpret int!: abelian_monoid \<Z> .
    7.49 +  then interpret int: abelian_monoid \<Z> .
    7.50  
    7.51    -- "Operations"
    7.52    { fix x y show "add \<Z> x y = x + y" by (simp add: int_ring_def) }
    7.53 @@ -164,7 +164,7 @@
    7.54    qed
    7.55  qed
    7.56  
    7.57 -interpretation int!: abelian_group \<Z>
    7.58 +interpretation int: abelian_group \<Z>
    7.59    where "a_inv \<Z> x = - x"
    7.60      and "a_minus \<Z> x y = x - y"
    7.61  proof -
    7.62 @@ -174,7 +174,7 @@
    7.63      show "!!x. x \<in> carrier \<Z> ==> EX y : carrier \<Z>. y \<oplus>\<^bsub>\<Z>\<^esub> x = \<zero>\<^bsub>\<Z>\<^esub>"
    7.64        by (simp add: int_ring_def) arith
    7.65    qed (auto simp: int_ring_def)
    7.66 -  then interpret int!: abelian_group \<Z> .
    7.67 +  then interpret int: abelian_group \<Z> .
    7.68  
    7.69    -- "Operations"
    7.70    { fix x y have "add \<Z> x y = x + y" by (simp add: int_ring_def) }
    7.71 @@ -187,7 +187,7 @@
    7.72    show "a_minus \<Z> x y = x - y" by (simp add: int.minus_eq add a_inv)
    7.73  qed
    7.74  
    7.75 -interpretation int!: "domain" \<Z>
    7.76 +interpretation int: "domain" \<Z>
    7.77    proof qed (auto simp: int_ring_def left_distrib right_distrib)
    7.78  
    7.79  
    7.80 @@ -203,7 +203,7 @@
    7.81    "(True ==> PROP R) == PROP R"
    7.82    by simp_all
    7.83  
    7.84 -interpretation int! (* FIXME [unfolded UNIV] *) :
    7.85 +interpretation int (* FIXME [unfolded UNIV] *) :
    7.86    partial_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
    7.87    where "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
    7.88      and "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
    7.89 @@ -219,7 +219,7 @@
    7.90      by (simp add: lless_def) auto
    7.91  qed
    7.92  
    7.93 -interpretation int! (* FIXME [unfolded UNIV] *) :
    7.94 +interpretation int (* FIXME [unfolded UNIV] *) :
    7.95    lattice "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
    7.96    where "join (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = max x y"
    7.97      and "meet (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = min x y"
    7.98 @@ -232,7 +232,7 @@
    7.99      apply (simp add: greatest_def Lower_def)
   7.100      apply arith
   7.101      done
   7.102 -  then interpret int!: lattice "?Z" .
   7.103 +  then interpret int: lattice "?Z" .
   7.104    show "join ?Z x y = max x y"
   7.105      apply (rule int.joinI)
   7.106      apply (simp_all add: least_def Upper_def)
   7.107 @@ -245,7 +245,7 @@
   7.108      done
   7.109  qed
   7.110  
   7.111 -interpretation int! (* [unfolded UNIV] *) :
   7.112 +interpretation int (* [unfolded UNIV] *) :
   7.113    total_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
   7.114    proof qed clarsimp
   7.115  

     8.1 --- a/src/HOL/Algebra/RingHom.thy	Thu Mar 26 19:24:21 2009 +0100
     8.2 +++ b/src/HOL/Algebra/RingHom.thy	Thu Mar 26 20:08:55 2009 +0100
     8.3 @@ -61,8 +61,8 @@
     8.4    assumes h: "h \<in> ring_hom R S"
     8.5    shows "ring_hom_ring R S h"
     8.6  proof -
     8.7 -  interpret R!: ring R by fact
     8.8 -  interpret S!: ring S by fact
     8.9 +  interpret R: ring R by fact
    8.10 +  interpret S: ring S by fact
    8.11    show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
    8.12      apply (rule R.is_ring)
    8.13      apply (rule S.is_ring)
    8.14 @@ -78,8 +78,8 @@
    8.15    shows "ring_hom_ring R S h"
    8.16  proof -
    8.17    interpret abelian_group_hom R S h by fact
    8.18 -  interpret R!: ring R by fact
    8.19 -  interpret S!: ring S by fact
    8.20 +  interpret R: ring R by fact
    8.21 +  interpret S: ring S by fact
    8.22    show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring)
    8.23      apply (insert group_hom.homh[OF a_group_hom])
    8.24      apply (unfold hom_def ring_hom_def, simp)
    8.25 @@ -94,8 +94,8 @@
    8.26    shows "ring_hom_cring R S h"
    8.27  proof -
    8.28    interpret ring_hom_ring R S h by fact
    8.29 -  interpret R!: cring R by fact
    8.30 -  interpret S!: cring S by fact
    8.31 +  interpret R: cring R by fact
    8.32 +  interpret S: cring S by fact
    8.33    show ?thesis by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro)
    8.34      (rule R.is_cring, rule S.is_cring, rule homh)
    8.35  qed

     9.1 --- a/src/HOL/Algebra/UnivPoly.thy	Thu Mar 26 19:24:21 2009 +0100
     9.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Thu Mar 26 20:08:55 2009 +0100
     9.3 @@ -1886,7 +1886,7 @@
     9.4    "UP INTEG"} globally.
     9.5  *}
     9.6  
     9.7 -interpretation INTEG!: UP_pre_univ_prop INTEG INTEG id "UP INTEG"
     9.8 +interpretation INTEG: UP_pre_univ_prop INTEG INTEG id "UP INTEG"
     9.9    using INTEG_id_eval by simp_all
    9.10  
    9.11  lemma INTEG_closed [intro, simp]:

    10.1 --- a/src/HOL/Complex.thy	Thu Mar 26 19:24:21 2009 +0100
    10.2 +++ b/src/HOL/Complex.thy	Thu Mar 26 20:08:55 2009 +0100
    10.3 @@ -348,13 +348,13 @@
    10.4  
    10.5  subsection {* Completeness of the Complexes *}
    10.6  
    10.7 -interpretation Re!: bounded_linear "Re"
    10.8 +interpretation Re: bounded_linear "Re"
    10.9  apply (unfold_locales, simp, simp)
   10.10  apply (rule_tac x=1 in exI)
   10.11  apply (simp add: complex_norm_def)
   10.12  done
   10.13  
   10.14 -interpretation Im!: bounded_linear "Im"
   10.15 +interpretation Im: bounded_linear "Im"
   10.16  apply (unfold_locales, simp, simp)
   10.17  apply (rule_tac x=1 in exI)
   10.18  apply (simp add: complex_norm_def)
   10.19 @@ -516,7 +516,7 @@
   10.20  lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<twosuperior>"
   10.21  by (simp add: norm_mult power2_eq_square)
   10.22  
   10.23 -interpretation cnj!: bounded_linear "cnj"
   10.24 +interpretation cnj: bounded_linear "cnj"
   10.25  apply (unfold_locales)
   10.26  apply (rule complex_cnj_add)
   10.27  apply (rule complex_cnj_scaleR)

    11.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Mar 26 19:24:21 2009 +0100
    11.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Mar 26 20:08:55 2009 +0100
    11.3 @@ -637,7 +637,7 @@
    11.4    using eq_diff_eq[where a= x and b=t and c=0] by simp
    11.5  
    11.6  
    11.7 -interpretation class_ordered_field_dense_linear_order!: constr_dense_linear_order
    11.8 +interpretation class_ordered_field_dense_linear_order: constr_dense_linear_order
    11.9   "op <=" "op <"
   11.10     "\<lambda> x y. 1/2 * ((x::'a::{ordered_field,recpower,number_ring}) + y)"
   11.11  proof (unfold_locales, dlo, dlo, auto)

    12.1 --- a/src/HOL/Divides.thy	Thu Mar 26 19:24:21 2009 +0100
    12.2 +++ b/src/HOL/Divides.thy	Thu Mar 26 20:08:55 2009 +0100
    12.3 @@ -852,7 +852,7 @@
    12.4  
    12.5  text {* @{term "op dvd"} is a partial order *}
    12.6  
    12.7 -interpretation dvd!: order "op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"
    12.8 +interpretation dvd: order "op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"
    12.9    proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym)
   12.10  
   12.11  lemma nat_dvd_diff[simp]: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"

    13.1 --- a/src/HOL/Finite_Set.thy	Thu Mar 26 19:24:21 2009 +0100
    13.2 +++ b/src/HOL/Finite_Set.thy	Thu Mar 26 20:08:55 2009 +0100
    13.3 @@ -928,7 +928,7 @@
    13.4  
    13.5  subsection {* Generalized summation over a set *}
    13.6  
    13.7 -interpretation comm_monoid_add!: comm_monoid_mult "0::'a::comm_monoid_add" "op +"
    13.8 +interpretation comm_monoid_add: comm_monoid_mult "0::'a::comm_monoid_add" "op +"
    13.9    proof qed (auto intro: add_assoc add_commute)
   13.10  
   13.11  definition setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"

    14.1 --- a/src/HOL/Groebner_Basis.thy	Thu Mar 26 19:24:21 2009 +0100
    14.2 +++ b/src/HOL/Groebner_Basis.thy	Thu Mar 26 20:08:55 2009 +0100
    14.3 @@ -163,7 +163,7 @@
    14.4  
    14.5  end
    14.6  
    14.7 -interpretation class_semiring!: gb_semiring
    14.8 +interpretation class_semiring: gb_semiring
    14.9      "op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"
   14.10    proof qed (auto simp add: algebra_simps power_Suc)
   14.11  
   14.12 @@ -242,7 +242,7 @@
   14.13  end
   14.14  
   14.15  
   14.16 -interpretation class_ring!: gb_ring "op +" "op *" "op ^"
   14.17 +interpretation class_ring: gb_ring "op +" "op *" "op ^"
   14.18      "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"
   14.19    proof qed simp_all
   14.20  
   14.21 @@ -343,7 +343,7 @@
   14.22    thus "b = 0" by blast
   14.23  qed
   14.24  
   14.25 -interpretation class_ringb!: ringb
   14.26 +interpretation class_ringb: ringb
   14.27    "op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"
   14.28  proof(unfold_locales, simp add: algebra_simps power_Suc, auto)
   14.29    fix w x y z ::"'a::{idom,recpower,number_ring}"
   14.30 @@ -359,7 +359,7 @@
   14.31  
   14.32  declaration {* normalizer_funs @{thm class_ringb.ringb_axioms'} *}
   14.33  
   14.34 -interpretation natgb!: semiringb
   14.35 +interpretation natgb: semiringb
   14.36    "op +" "op *" "op ^" "0::nat" "1"
   14.37  proof (unfold_locales, simp add: algebra_simps power_Suc)
   14.38    fix w x y z ::"nat"
   14.39 @@ -463,7 +463,7 @@
   14.40  
   14.41  subsection{* Groebner Bases for fields *}
   14.42  
   14.43 -interpretation class_fieldgb!:
   14.44 +interpretation class_fieldgb:
   14.45    fieldgb "op +" "op *" "op ^" "0::'a::{field,recpower,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse)
   14.46  
   14.47  lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp

    15.1 --- a/src/HOL/HahnBanach/Subspace.thy	Thu Mar 26 19:24:21 2009 +0100
    15.2 +++ b/src/HOL/HahnBanach/Subspace.thy	Thu Mar 26 20:08:55 2009 +0100
    15.3 @@ -59,7 +59,7 @@
    15.4    assumes "vectorspace V"
    15.5    shows "0 \<in> U"
    15.6  proof -
    15.7 -  interpret V!: vectorspace V by fact
    15.8 +  interpret V: vectorspace V by fact
    15.9    have "U \<noteq> {}" by (rule non_empty)
   15.10    then obtain x where x: "x \<in> U" by blast
   15.11    then have "x \<in> V" .. then have "0 = x - x" by simp

    16.1 --- a/src/HOL/Lattices.thy	Thu Mar 26 19:24:21 2009 +0100
    16.2 +++ b/src/HOL/Lattices.thy	Thu Mar 26 20:08:55 2009 +0100
    16.3 @@ -299,7 +299,7 @@
    16.4    by auto
    16.5  qed (auto simp add: min_def max_def not_le less_imp_le)
    16.6  
    16.7 -interpretation min_max!: distrib_lattice "op \<le> :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max
    16.8 +interpretation min_max: distrib_lattice "op \<le> :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max
    16.9    by (rule distrib_lattice_min_max)
   16.10  
   16.11  lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{lower_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"

    17.1 --- a/src/HOL/Library/FrechetDeriv.thy	Thu Mar 26 19:24:21 2009 +0100
    17.2 +++ b/src/HOL/Library/FrechetDeriv.thy	Thu Mar 26 20:08:55 2009 +0100
    17.3 @@ -222,8 +222,8 @@
    17.4    let ?k = "\<lambda>h. f (x + h) - f x"
    17.5    let ?Nf = "\<lambda>h. norm (?Rf h) / norm h"
    17.6    let ?Ng = "\<lambda>h. norm (?Rg (?k h)) / norm (?k h)"
    17.7 -  from f interpret F!: bounded_linear "F" by (rule FDERIV_bounded_linear)
    17.8 -  from g interpret G!: bounded_linear "G" by (rule FDERIV_bounded_linear)
    17.9 +  from f interpret F: bounded_linear "F" by (rule FDERIV_bounded_linear)
   17.10 +  from g interpret G: bounded_linear "G" by (rule FDERIV_bounded_linear)
   17.11    from F.bounded obtain kF where kF: "\<And>x. norm (F x) \<le> norm x * kF" by fast
   17.12    from G.bounded obtain kG where kG: "\<And>x. norm (G x) \<le> norm x * kG" by fast
   17.13  

    18.1 --- a/src/HOL/Library/Inner_Product.thy	Thu Mar 26 19:24:21 2009 +0100
    18.2 +++ b/src/HOL/Library/Inner_Product.thy	Thu Mar 26 20:08:55 2009 +0100
    18.3 @@ -116,7 +116,7 @@
    18.4  
    18.5  end
    18.6  
    18.7 -interpretation inner!:
    18.8 +interpretation inner:
    18.9    bounded_bilinear "inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real"
   18.10  proof
   18.11    fix x y z :: 'a and r :: real
   18.12 @@ -135,11 +135,11 @@
   18.13    qed
   18.14  qed
   18.15  
   18.16 -interpretation inner_left!:
   18.17 +interpretation inner_left:
   18.18    bounded_linear "\<lambda>x::'a::real_inner. inner x y"
   18.19    by (rule inner.bounded_linear_left)
   18.20  
   18.21 -interpretation inner_right!:
   18.22 +interpretation inner_right:
   18.23    bounded_linear "\<lambda>y::'a::real_inner. inner x y"
   18.24    by (rule inner.bounded_linear_right)
   18.25  

    19.1 --- a/src/HOL/Library/Multiset.thy	Thu Mar 26 19:24:21 2009 +0100
    19.2 +++ b/src/HOL/Library/Multiset.thy	Thu Mar 26 20:08:55 2009 +0100
    19.3 @@ -1077,15 +1077,15 @@
    19.4  apply simp
    19.5  done
    19.6  
    19.7 -interpretation mset_order!: order "op \<le>#" "op <#"
    19.8 +interpretation mset_order: order "op \<le>#" "op <#"
    19.9  proof qed (auto intro: order.intro mset_le_refl mset_le_antisym
   19.10    mset_le_trans simp: mset_less_def)
   19.11  
   19.12 -interpretation mset_order_cancel_semigroup!:
   19.13 +interpretation mset_order_cancel_semigroup:
   19.14    pordered_cancel_ab_semigroup_add "op +" "op \<le>#" "op <#"
   19.15  proof qed (erule mset_le_mono_add [OF mset_le_refl])
   19.16  
   19.17 -interpretation mset_order_semigroup_cancel!:
   19.18 +interpretation mset_order_semigroup_cancel:
   19.19    pordered_ab_semigroup_add_imp_le "op +" "op \<le>#" "op <#"
   19.20  proof qed simp
   19.21  
   19.22 @@ -1433,7 +1433,7 @@
   19.23  definition [code del]:
   19.24   "image_mset f = fold_mset (op + o single o f) {#}"
   19.25  
   19.26 -interpretation image_left_comm!: left_commutative "op + o single o f"
   19.27 +interpretation image_left_comm: left_commutative "op + o single o f"
   19.28    proof qed (simp add:union_ac)
   19.29  
   19.30  lemma image_mset_empty [simp]: "image_mset f {#} = {#}"

    20.1 --- a/src/HOL/Library/Numeral_Type.thy	Thu Mar 26 19:24:21 2009 +0100
    20.2 +++ b/src/HOL/Library/Numeral_Type.thy	Thu Mar 26 20:08:55 2009 +0100
    20.3 @@ -313,7 +313,7 @@
    20.4  
    20.5  end
    20.6  
    20.7 -interpretation bit0!:
    20.8 +interpretation bit0:
    20.9    mod_type "int CARD('a::finite bit0)"
   20.10             "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
   20.11             "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
   20.12 @@ -329,7 +329,7 @@
   20.13  apply (rule power_bit0_def [unfolded Abs_bit0'_def])
   20.14  done
   20.15  
   20.16 -interpretation bit1!:
   20.17 +interpretation bit1:
   20.18    mod_type "int CARD('a::finite bit1)"
   20.19             "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
   20.20             "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
   20.21 @@ -363,13 +363,13 @@
   20.22  
   20.23  end
   20.24  
   20.25 -interpretation bit0!:
   20.26 +interpretation bit0:
   20.27    mod_ring "int CARD('a::finite bit0)"
   20.28             "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
   20.29             "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
   20.30    ..
   20.31  
   20.32 -interpretation bit1!:
   20.33 +interpretation bit1:
   20.34    mod_ring "int CARD('a::finite bit1)"
   20.35             "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
   20.36             "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"

    21.1 --- a/src/HOL/Library/Product_Vector.thy	Thu Mar 26 19:24:21 2009 +0100
    21.2 +++ b/src/HOL/Library/Product_Vector.thy	Thu Mar 26 20:08:55 2009 +0100
    21.3 @@ -116,14 +116,14 @@
    21.4  
    21.5  subsection {* Pair operations are linear and continuous *}
    21.6  
    21.7 -interpretation fst!: bounded_linear fst
    21.8 +interpretation fst: bounded_linear fst
    21.9    apply (unfold_locales)
   21.10    apply (rule fst_add)
   21.11    apply (rule fst_scaleR)
   21.12    apply (rule_tac x="1" in exI, simp add: norm_Pair)
   21.13    done
   21.14  
   21.15 -interpretation snd!: bounded_linear snd
   21.16 +interpretation snd: bounded_linear snd
   21.17    apply (unfold_locales)
   21.18    apply (rule snd_add)
   21.19    apply (rule snd_scaleR)

    22.1 --- a/src/HOL/Library/SetsAndFunctions.thy	Thu Mar 26 19:24:21 2009 +0100
    22.2 +++ b/src/HOL/Library/SetsAndFunctions.thy	Thu Mar 26 20:08:55 2009 +0100
    22.3 @@ -107,26 +107,26 @@
    22.4    apply simp
    22.5    done
    22.6  
    22.7 -interpretation set_semigroup_add!: semigroup_add "op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"
    22.8 +interpretation set_semigroup_add: semigroup_add "op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"
    22.9    apply default
   22.10    apply (unfold set_plus_def)
   22.11    apply (force simp add: add_assoc)
   22.12    done
   22.13  
   22.14 -interpretation set_semigroup_mult!: semigroup_mult "op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"
   22.15 +interpretation set_semigroup_mult: semigroup_mult "op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"
   22.16    apply default
   22.17    apply (unfold set_times_def)
   22.18    apply (force simp add: mult_assoc)
   22.19    done
   22.20  
   22.21 -interpretation set_comm_monoid_add!: comm_monoid_add "{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"
   22.22 +interpretation set_comm_monoid_add: comm_monoid_add "{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"
   22.23    apply default
   22.24     apply (unfold set_plus_def)
   22.25     apply (force simp add: add_ac)
   22.26    apply force
   22.27    done
   22.28  
   22.29 -interpretation set_comm_monoid_mult!: comm_monoid_mult "{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"
   22.30 +interpretation set_comm_monoid_mult: comm_monoid_mult "{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"
   22.31    apply default
   22.32     apply (unfold set_times_def)
   22.33     apply (force simp add: mult_ac)

    23.1 --- a/src/HOL/NSA/StarDef.thy	Thu Mar 26 19:24:21 2009 +0100
    23.2 +++ b/src/HOL/NSA/StarDef.thy	Thu Mar 26 20:08:55 2009 +0100
    23.3 @@ -23,7 +23,7 @@
    23.4  apply (rule nat_infinite)
    23.5  done
    23.6  
    23.7 -interpretation FreeUltrafilterNat!: freeultrafilter FreeUltrafilterNat
    23.8 +interpretation FreeUltrafilterNat: freeultrafilter FreeUltrafilterNat
    23.9  by (rule freeultrafilter_FreeUltrafilterNat)
   23.10  
   23.11  text {* This rule takes the place of the old ultra tactic *}

    24.1 --- a/src/HOL/RealVector.thy	Thu Mar 26 19:24:21 2009 +0100
    24.2 +++ b/src/HOL/RealVector.thy	Thu Mar 26 20:08:55 2009 +0100
    24.3 @@ -145,7 +145,7 @@
    24.4    and scaleR_scaleR: "scaleR a (scaleR b x) = scaleR (a * b) x"
    24.5    and scaleR_one: "scaleR 1 x = x"
    24.6  
    24.7 -interpretation real_vector!:
    24.8 +interpretation real_vector:
    24.9    vector_space "scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"
   24.10  apply unfold_locales
   24.11  apply (rule scaleR_right_distrib)
   24.12 @@ -190,10 +190,10 @@
   24.13  
   24.14  end
   24.15  
   24.16 -interpretation scaleR_left!: additive "(\<lambda>a. scaleR a x::'a::real_vector)"
   24.17 +interpretation scaleR_left: additive "(\<lambda>a. scaleR a x::'a::real_vector)"
   24.18  proof qed (rule scaleR_left_distrib)
   24.19  
   24.20 -interpretation scaleR_right!: additive "(\<lambda>x. scaleR a x::'a::real_vector)"
   24.21 +interpretation scaleR_right: additive "(\<lambda>x. scaleR a x::'a::real_vector)"
   24.22  proof qed (rule scaleR_right_distrib)
   24.23  
   24.24  lemma nonzero_inverse_scaleR_distrib:
   24.25 @@ -789,7 +789,7 @@
   24.26  
   24.27  end
   24.28  
   24.29 -interpretation mult!:
   24.30 +interpretation mult:
   24.31    bounded_bilinear "op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"
   24.32  apply (rule bounded_bilinear.intro)
   24.33  apply (rule left_distrib)
   24.34 @@ -800,19 +800,19 @@
   24.35  apply (simp add: norm_mult_ineq)
   24.36  done
   24.37  
   24.38 -interpretation mult_left!:
   24.39 +interpretation mult_left:
   24.40    bounded_linear "(\<lambda>x::'a::real_normed_algebra. x * y)"
   24.41  by (rule mult.bounded_linear_left)
   24.42  
   24.43 -interpretation mult_right!:
   24.44 +interpretation mult_right:
   24.45    bounded_linear "(\<lambda>y::'a::real_normed_algebra. x * y)"
   24.46  by (rule mult.bounded_linear_right)
   24.47  
   24.48 -interpretation divide!:
   24.49 +interpretation divide:
   24.50    bounded_linear "(\<lambda>x::'a::real_normed_field. x / y)"
   24.51  unfolding divide_inverse by (rule mult.bounded_linear_left)
   24.52  
   24.53 -interpretation scaleR!: bounded_bilinear "scaleR"
   24.54 +interpretation scaleR: bounded_bilinear "scaleR"
   24.55  apply (rule bounded_bilinear.intro)
   24.56  apply (rule scaleR_left_distrib)
   24.57  apply (rule scaleR_right_distrib)
   24.58 @@ -822,13 +822,13 @@
   24.59  apply (simp add: norm_scaleR)
   24.60  done
   24.61  
   24.62 -interpretation scaleR_left!: bounded_linear "\<lambda>r. scaleR r x"
   24.63 +interpretation scaleR_left: bounded_linear "\<lambda>r. scaleR r x"
   24.64  by (rule scaleR.bounded_linear_left)
   24.65  
   24.66 -interpretation scaleR_right!: bounded_linear "\<lambda>x. scaleR r x"
   24.67 +interpretation scaleR_right: bounded_linear "\<lambda>x. scaleR r x"
   24.68  by (rule scaleR.bounded_linear_right)
   24.69  
   24.70 -interpretation of_real!: bounded_linear "\<lambda>r. of_real r"
   24.71 +interpretation of_real: bounded_linear "\<lambda>r. of_real r"
   24.72  unfolding of_real_def by (rule scaleR.bounded_linear_left)
   24.73  
   24.74  end

    25.1 --- a/src/HOL/Word/TdThs.thy	Thu Mar 26 19:24:21 2009 +0100
    25.2 +++ b/src/HOL/Word/TdThs.thy	Thu Mar 26 20:08:55 2009 +0100
    25.3 @@ -89,7 +89,7 @@
    25.4  
    25.5  end
    25.6  
    25.7 -interpretation nat_int!: type_definition int nat "Collect (op <= 0)"
    25.8 +interpretation nat_int: type_definition int nat "Collect (op <= 0)"
    25.9    by (rule td_nat_int)
   25.10  
   25.11  declare

    26.1 --- a/src/HOL/Word/WordArith.thy	Thu Mar 26 19:24:21 2009 +0100
    26.2 +++ b/src/HOL/Word/WordArith.thy	Thu Mar 26 20:08:55 2009 +0100
    26.3 @@ -21,7 +21,7 @@
    26.4  proof
    26.5  qed (unfold word_sle_def word_sless_def, auto)
    26.6  
    26.7 -interpretation signed!: linorder "word_sle" "word_sless"
    26.8 +interpretation signed: linorder "word_sle" "word_sless"
    26.9    by (rule signed_linorder)
   26.10  
   26.11  lemmas word_arith_wis = 
   26.12 @@ -862,7 +862,7 @@
   26.13  lemmas td_ext_unat = refl [THEN td_ext_unat']
   26.14  lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm, standard]
   26.15  
   26.16 -interpretation word_unat!:
   26.17 +interpretation word_unat:
   26.18    td_ext "unat::'a::len word => nat" 
   26.19           of_nat 
   26.20           "unats (len_of TYPE('a::len))"

    27.1 --- a/src/HOL/Word/WordBitwise.thy	Thu Mar 26 19:24:21 2009 +0100
    27.2 +++ b/src/HOL/Word/WordBitwise.thy	Thu Mar 26 20:08:55 2009 +0100
    27.3 @@ -343,7 +343,7 @@
    27.4  
    27.5  lemmas td_ext_nth = td_ext_nth' [OF refl refl refl, unfolded word_size]
    27.6  
    27.7 -interpretation test_bit!:
    27.8 +interpretation test_bit:
    27.9    td_ext "op !! :: 'a::len0 word => nat => bool"
   27.10           set_bits
   27.11           "{f. \<forall>i. f i \<longrightarrow> i < len_of TYPE('a::len0)}"

    28.1 --- a/src/HOL/Word/WordDefinition.thy	Thu Mar 26 19:24:21 2009 +0100
    28.2 +++ b/src/HOL/Word/WordDefinition.thy	Thu Mar 26 20:08:55 2009 +0100
    28.3 @@ -351,7 +351,7 @@
    28.4  
    28.5  lemmas int_word_uint = td_ext_uint [THEN td_ext.eq_norm, standard]
    28.6  
    28.7 -interpretation word_uint!:
    28.8 +interpretation word_uint:
    28.9    td_ext "uint::'a::len0 word \<Rightarrow> int" 
   28.10           word_of_int 
   28.11           "uints (len_of TYPE('a::len0))"
   28.12 @@ -363,7 +363,7 @@
   28.13  lemmas td_ext_ubin = td_ext_uint 
   28.14    [simplified len_gt_0 no_bintr_alt1 [symmetric]]
   28.15  
   28.16 -interpretation word_ubin!:
   28.17 +interpretation word_ubin:
   28.18    td_ext "uint::'a::len0 word \<Rightarrow> int" 
   28.19           word_of_int 
   28.20           "uints (len_of TYPE('a::len0))"
   28.21 @@ -418,7 +418,7 @@
   28.22     and interpretations do not produce thm duplicates. I.e. 
   28.23     we get the name word_sint.Rep_eqD, but not word_sbin.Req_eqD,
   28.24     because the latter is the same thm as the former *)
   28.25 -interpretation word_sint!:
   28.26 +interpretation word_sint:
   28.27    td_ext "sint ::'a::len word => int" 
   28.28            word_of_int 
   28.29            "sints (len_of TYPE('a::len))"
   28.30 @@ -426,7 +426,7 @@
   28.31                 2 ^ (len_of TYPE('a::len) - 1)"
   28.32    by (rule td_ext_sint)
   28.33  
   28.34 -interpretation word_sbin!:
   28.35 +interpretation word_sbin:
   28.36    td_ext "sint ::'a::len word => int" 
   28.37            word_of_int 
   28.38            "sints (len_of TYPE('a::len))"
   28.39 @@ -630,7 +630,7 @@
   28.40    apply simp
   28.41    done
   28.42  
   28.43 -interpretation word_bl!:
   28.44 +interpretation word_bl:
   28.45    type_definition "to_bl :: 'a::len0 word => bool list"
   28.46                    of_bl  
   28.47                    "{bl. length bl = len_of TYPE('a::len0)}"

    29.1 --- a/src/HOL/Word/WordGenLib.thy	Thu Mar 26 19:24:21 2009 +0100
    29.2 +++ b/src/HOL/Word/WordGenLib.thy	Thu Mar 26 20:08:55 2009 +0100
    29.3 @@ -106,7 +106,7 @@
    29.4    apply (rule word_or_not)
    29.5    done
    29.6  
    29.7 -interpretation word_bool_alg!:
    29.8 +interpretation word_bool_alg:
    29.9    boolean "op AND" "op OR" bitNOT 0 max_word
   29.10    by (rule word_boolean)
   29.11  
   29.12 @@ -114,7 +114,7 @@
   29.13    "x XOR y = x AND NOT y OR NOT x AND (y::'a::len0 word)"
   29.14    by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
   29.15  
   29.16 -interpretation word_bool_alg!:
   29.17 +interpretation word_bool_alg:
   29.18    boolean_xor "op AND" "op OR" bitNOT 0 max_word "op XOR"
   29.19    apply (rule boolean_xor.intro)
   29.20     apply (rule word_boolean)

    30.1 --- a/src/HOL/ex/LocaleTest2.thy	Thu Mar 26 19:24:21 2009 +0100
    30.2 +++ b/src/HOL/ex/LocaleTest2.thy	Thu Mar 26 20:08:55 2009 +0100
    30.3 @@ -468,7 +468,7 @@
    30.4  
    30.5  subsubsection {* Total order @{text "<="} on @{typ int} *}
    30.6  
    30.7 -interpretation int!: dpo "op <= :: [int, int] => bool"
    30.8 +interpretation int: dpo "op <= :: [int, int] => bool"
    30.9    where "(dpo.less (op <=) (x::int) y) = (x < y)"
   30.10    txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
   30.11  proof -
   30.12 @@ -487,7 +487,7 @@
   30.13  lemma "(op < :: [int, int] => bool) = op <"
   30.14    apply (rule int.abs_test) done
   30.15  
   30.16 -interpretation int!: dlat "op <= :: [int, int] => bool"
   30.17 +interpretation int: dlat "op <= :: [int, int] => bool"
   30.18    where meet_eq: "dlat.meet (op <=) (x::int) y = min x y"
   30.19      and join_eq: "dlat.join (op <=) (x::int) y = max x y"
   30.20  proof -
   30.21 @@ -511,7 +511,7 @@
   30.22      by auto
   30.23  qed
   30.24  
   30.25 -interpretation int!: dlo "op <= :: [int, int] => bool"
   30.26 +interpretation int: dlo "op <= :: [int, int] => bool"
   30.27    proof qed arith
   30.28  
   30.29  text {* Interpreted theorems from the locales, involving defined terms. *}
   30.30 @@ -524,7 +524,7 @@
   30.31  
   30.32  subsubsection {* Total order @{text "<="} on @{typ nat} *}
   30.33  
   30.34 -interpretation nat!: dpo "op <= :: [nat, nat] => bool"
   30.35 +interpretation nat: dpo "op <= :: [nat, nat] => bool"
   30.36    where "dpo.less (op <=) (x::nat) y = (x < y)"
   30.37    txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
   30.38  proof -
   30.39 @@ -538,7 +538,7 @@
   30.40      done
   30.41  qed
   30.42  
   30.43 -interpretation nat!: dlat "op <= :: [nat, nat] => bool"
   30.44 +interpretation nat: dlat "op <= :: [nat, nat] => bool"
   30.45    where "dlat.meet (op <=) (x::nat) y = min x y"
   30.46      and "dlat.join (op <=) (x::nat) y = max x y"
   30.47  proof -
   30.48 @@ -562,7 +562,7 @@
   30.49      by auto
   30.50  qed
   30.51  
   30.52 -interpretation nat!: dlo "op <= :: [nat, nat] => bool"
   30.53 +interpretation nat: dlo "op <= :: [nat, nat] => bool"
   30.54    proof qed arith
   30.55  
   30.56  text {* Interpreted theorems from the locales, involving defined terms. *}
   30.57 @@ -575,7 +575,7 @@
   30.58  
   30.59  subsubsection {* Lattice @{text "dvd"} on @{typ nat} *}
   30.60  
   30.61 -interpretation nat_dvd!: dpo "op dvd :: [nat, nat] => bool"
   30.62 +interpretation nat_dvd: dpo "op dvd :: [nat, nat] => bool"
   30.63    where "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
   30.64    txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
   30.65  proof -
   30.66 @@ -589,7 +589,7 @@
   30.67      done
   30.68  qed
   30.69  
   30.70 -interpretation nat_dvd!: dlat "op dvd :: [nat, nat] => bool"
   30.71 +interpretation nat_dvd: dlat "op dvd :: [nat, nat] => bool"
   30.72    where "dlat.meet (op dvd) (x::nat) y = gcd x y"
   30.73      and "dlat.join (op dvd) (x::nat) y = lcm x y"
   30.74  proof -
   30.75 @@ -834,7 +834,7 @@
   30.76  
   30.77  subsubsection {* Interpretation of Functions *}
   30.78  
   30.79 -interpretation Dfun!: Dmonoid "op o" "id :: 'a => 'a"
   30.80 +interpretation Dfun: Dmonoid "op o" "id :: 'a => 'a"
   30.81    where "Dmonoid.unit (op o) id f = bij (f::'a => 'a)"
   30.82  (*    and "Dmonoid.inv (op o) id" = "inv :: ('a => 'a) => ('a => 'a)" *)
   30.83  proof -
   30.84 @@ -884,7 +884,7 @@
   30.85    "(f :: unit => unit) = id"
   30.86    by rule simp
   30.87  
   30.88 -interpretation Dfun!: Dgrp "op o" "id :: unit => unit"
   30.89 +interpretation Dfun: Dgrp "op o" "id :: unit => unit"
   30.90    where "Dmonoid.inv (op o) id f = inv (f :: unit => unit)"
   30.91  proof -
   30.92    have "Dmonoid op o (id :: 'a => 'a)" ..

    31.1 --- a/src/HOLCF/Algebraic.thy	Thu Mar 26 19:24:21 2009 +0100
    31.2 +++ b/src/HOLCF/Algebraic.thy	Thu Mar 26 20:08:55 2009 +0100
    31.3 @@ -215,7 +215,7 @@
    31.4  lemma finite_deflation_Rep_fin_defl: "finite_deflation (Rep_fin_defl d)"
    31.5  using Rep_fin_defl by simp
    31.6  
    31.7 -interpretation Rep_fin_defl!: finite_deflation "Rep_fin_defl d"
    31.8 +interpretation Rep_fin_defl: finite_deflation "Rep_fin_defl d"
    31.9  by (rule finite_deflation_Rep_fin_defl)
   31.10  
   31.11  lemma fin_defl_lessI:
   31.12 @@ -320,7 +320,7 @@
   31.13  apply (rule Rep_fin_defl.compact)
   31.14  done
   31.15  
   31.16 -interpretation fin_defl!: basis_take sq_le fd_take
   31.17 +interpretation fin_defl: basis_take sq_le fd_take
   31.18  apply default
   31.19  apply (rule fd_take_less)
   31.20  apply (rule fd_take_idem)
   31.21 @@ -370,7 +370,7 @@
   31.22  unfolding alg_defl_principal_def
   31.23  by (simp add: Abs_alg_defl_inverse sq_le.ideal_principal)
   31.24  
   31.25 -interpretation alg_defl!:
   31.26 +interpretation alg_defl:
   31.27    ideal_completion sq_le fd_take alg_defl_principal Rep_alg_defl
   31.28  apply default
   31.29  apply (rule ideal_Rep_alg_defl)
   31.30 @@ -461,7 +461,7 @@
   31.31  apply (rule finite_deflation_Rep_fin_defl)
   31.32  done
   31.33  
   31.34 -interpretation cast!: deflation "cast\<cdot>d"
   31.35 +interpretation cast: deflation "cast\<cdot>d"
   31.36  by (rule deflation_cast)
   31.37  
   31.38  lemma "cast\<cdot>(\<Squnion>i. alg_defl_principal (Abs_fin_defl (approx i)))\<cdot>x = x"

    32.1 --- a/src/HOLCF/Bifinite.thy	Thu Mar 26 19:24:21 2009 +0100
    32.2 +++ b/src/HOLCF/Bifinite.thy	Thu Mar 26 20:08:55 2009 +0100
    32.3 @@ -37,7 +37,7 @@
    32.4      by (rule finite_fixes_approx)
    32.5  qed
    32.6  
    32.7 -interpretation approx!: finite_deflation "approx i"
    32.8 +interpretation approx: finite_deflation "approx i"
    32.9  by (rule finite_deflation_approx)
   32.10  
   32.11  lemma (in deflation) deflation: "deflation d" ..

    33.1 --- a/src/HOLCF/CompactBasis.thy	Thu Mar 26 19:24:21 2009 +0100
    33.2 +++ b/src/HOLCF/CompactBasis.thy	Thu Mar 26 20:08:55 2009 +0100
    33.3 @@ -46,7 +46,7 @@
    33.4  
    33.5  lemmas approx_Rep_compact_basis = Rep_compact_take [symmetric]
    33.6  
    33.7 -interpretation compact_basis!:
    33.8 +interpretation compact_basis:
    33.9    basis_take sq_le compact_take
   33.10  proof
   33.11    fix n :: nat and a :: "'a compact_basis"
   33.12 @@ -92,7 +92,7 @@
   33.13    approximants :: "'a \<Rightarrow> 'a compact_basis set" where
   33.14    "approximants = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
   33.15  
   33.16 -interpretation compact_basis!:
   33.17 +interpretation compact_basis:
   33.18    ideal_completion sq_le compact_take Rep_compact_basis approximants
   33.19  proof
   33.20    fix w :: 'a

    34.1 --- a/src/HOLCF/Completion.thy	Thu Mar 26 19:24:21 2009 +0100
    34.2 +++ b/src/HOLCF/Completion.thy	Thu Mar 26 20:08:55 2009 +0100
    34.3 @@ -156,7 +156,7 @@
    34.4  
    34.5  end
    34.6  
    34.7 -interpretation sq_le!: preorder "sq_le :: 'a::po \<Rightarrow> 'a \<Rightarrow> bool"
    34.8 +interpretation sq_le: preorder "sq_le :: 'a::po \<Rightarrow> 'a \<Rightarrow> bool"
    34.9  apply unfold_locales
   34.10  apply (rule refl_less)
   34.11  apply (erule (1) trans_less)

    35.1 --- a/src/HOLCF/ConvexPD.thy	Thu Mar 26 19:24:21 2009 +0100
    35.2 +++ b/src/HOLCF/ConvexPD.thy	Thu Mar 26 20:08:55 2009 +0100
    35.3 @@ -20,7 +20,7 @@
    35.4  lemma convex_le_trans: "\<lbrakk>t \<le>\<natural> u; u \<le>\<natural> v\<rbrakk> \<Longrightarrow> t \<le>\<natural> v"
    35.5  unfolding convex_le_def by (fast intro: upper_le_trans lower_le_trans)
    35.6  
    35.7 -interpretation convex_le!: preorder convex_le
    35.8 +interpretation convex_le: preorder convex_le
    35.9  by (rule preorder.intro, rule convex_le_refl, rule convex_le_trans)
   35.10  
   35.11  lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<natural> t"
   35.12 @@ -178,7 +178,7 @@
   35.13  unfolding convex_principal_def
   35.14  by (simp add: Abs_convex_pd_inverse convex_le.ideal_principal)
   35.15  
   35.16 -interpretation convex_pd!:
   35.17 +interpretation convex_pd:
   35.18    ideal_completion convex_le pd_take convex_principal Rep_convex_pd
   35.19  apply unfold_locales
   35.20  apply (rule pd_take_convex_le)

    36.1 --- a/src/HOLCF/LowerPD.thy	Thu Mar 26 19:24:21 2009 +0100
    36.2 +++ b/src/HOLCF/LowerPD.thy	Thu Mar 26 20:08:55 2009 +0100
    36.3 @@ -26,7 +26,7 @@
    36.4  apply (erule (1) trans_less)
    36.5  done
    36.6  
    36.7 -interpretation lower_le!: preorder lower_le
    36.8 +interpretation lower_le: preorder lower_le
    36.9  by (rule preorder.intro, rule lower_le_refl, rule lower_le_trans)
   36.10  
   36.11  lemma lower_le_minimal [simp]: "PDUnit compact_bot \<le>\<flat> t"
   36.12 @@ -133,7 +133,7 @@
   36.13  unfolding lower_principal_def
   36.14  by (simp add: Abs_lower_pd_inverse lower_le.ideal_principal)
   36.15  
   36.16 -interpretation lower_pd!:
   36.17 +interpretation lower_pd:
   36.18    ideal_completion lower_le pd_take lower_principal Rep_lower_pd
   36.19  apply unfold_locales
   36.20  apply (rule pd_take_lower_le)

    37.1 --- a/src/HOLCF/Universal.thy	Thu Mar 26 19:24:21 2009 +0100
    37.2 +++ b/src/HOLCF/Universal.thy	Thu Mar 26 20:08:55 2009 +0100
    37.3 @@ -230,13 +230,13 @@
    37.4  apply (simp add: ubasis_take_same)
    37.5  done
    37.6  
    37.7 -interpretation udom!: preorder ubasis_le
    37.8 +interpretation udom: preorder ubasis_le
    37.9  apply default
   37.10  apply (rule ubasis_le_refl)
   37.11  apply (erule (1) ubasis_le_trans)
   37.12  done
   37.13  
   37.14 -interpretation udom!: basis_take ubasis_le ubasis_take
   37.15 +interpretation udom: basis_take ubasis_le ubasis_take
   37.16  apply default
   37.17  apply (rule ubasis_take_less)
   37.18  apply (rule ubasis_take_idem)
   37.19 @@ -285,7 +285,7 @@
   37.20  unfolding udom_principal_def
   37.21  by (simp add: Abs_udom_inverse udom.ideal_principal)
   37.22  
   37.23 -interpretation udom!:
   37.24 +interpretation udom:
   37.25    ideal_completion ubasis_le ubasis_take udom_principal Rep_udom
   37.26  apply unfold_locales
   37.27  apply (rule ideal_Rep_udom)

    38.1 --- a/src/HOLCF/UpperPD.thy	Thu Mar 26 19:24:21 2009 +0100
    38.2 +++ b/src/HOLCF/UpperPD.thy	Thu Mar 26 20:08:55 2009 +0100
    38.3 @@ -26,7 +26,7 @@
    38.4  apply (erule (1) trans_less)
    38.5  done
    38.6  
    38.7 -interpretation upper_le!: preorder upper_le
    38.8 +interpretation upper_le: preorder upper_le
    38.9  by (rule preorder.intro, rule upper_le_refl, rule upper_le_trans)
   38.10  
   38.11  lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<sharp> t"
   38.12 @@ -131,7 +131,7 @@
   38.13  unfolding upper_principal_def
   38.14  by (simp add: Abs_upper_pd_inverse upper_le.ideal_principal)
   38.15  
   38.16 -interpretation upper_pd!:
   38.17 +interpretation upper_pd:
   38.18    ideal_completion upper_le pd_take upper_principal Rep_upper_pd
   38.19  apply unfold_locales
   38.20  apply (rule pd_take_upper_le)

    39.1 --- a/src/ZF/Constructible/L_axioms.thy	Thu Mar 26 19:24:21 2009 +0100
    39.2 +++ b/src/ZF/Constructible/L_axioms.thy	Thu Mar 26 20:08:55 2009 +0100
    39.3 @@ -99,7 +99,7 @@
    39.4    apply (rule L_nat)
    39.5    done
    39.6  
    39.7 -interpretation L: M_trivial L by (rule M_trivial_L)
    39.8 +interpretation L?: M_trivial L by (rule M_trivial_L)
    39.9  
   39.10  (* Replaces the following declarations...
   39.11  lemmas rall_abs = M_trivial.rall_abs [OF M_trivial_L]

    40.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Thu Mar 26 19:24:21 2009 +0100
    40.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Thu Mar 26 20:08:55 2009 +0100
    40.3 @@ -185,7 +185,7 @@
    40.4  theorem M_trancl_L: "PROP M_trancl(L)"
    40.5  by (rule M_trancl.intro [OF M_basic_L M_trancl_axioms_L])
    40.6  
    40.7 -interpretation L: M_trancl L by (rule M_trancl_L)
    40.8 +interpretation L?: M_trancl L by (rule M_trancl_L)
    40.9  
   40.10  
   40.11  subsection{*@{term L} is Closed Under the Operator @{term list}*}
   40.12 @@ -372,7 +372,7 @@
   40.13    apply (rule M_datatypes_axioms_L) 
   40.14    done
   40.15  
   40.16 -interpretation L: M_datatypes L by (rule M_datatypes_L)
   40.17 +interpretation L?: M_datatypes L by (rule M_datatypes_L)
   40.18  
   40.19  
   40.20  subsection{*@{term L} is Closed Under the Operator @{term eclose}*}
   40.21 @@ -435,7 +435,7 @@
   40.22    apply (rule M_eclose_axioms_L)
   40.23    done
   40.24  
   40.25 -interpretation L: M_eclose L by (rule M_eclose_L)
   40.26 +interpretation L?: M_eclose L by (rule M_eclose_L)
   40.27  
   40.28  
   40.29  end

    41.1 --- a/src/ZF/Constructible/Separation.thy	Thu Mar 26 19:24:21 2009 +0100
    41.2 +++ b/src/ZF/Constructible/Separation.thy	Thu Mar 26 20:08:55 2009 +0100
    41.3 @@ -305,7 +305,7 @@
    41.4  theorem M_basic_L: "PROP M_basic(L)"
    41.5  by (rule M_basic.intro [OF M_trivial_L M_basic_axioms_L])
    41.6  
    41.7 -interpretation L: M_basic L by (rule M_basic_L)
    41.8 +interpretation L?: M_basic L by (rule M_basic_L)
    41.9  
   41.10  
   41.11  end