src/HOL/ex/LocaleTest2.thy

--- a/src/HOL/ex/LocaleTest2.thy	Sun Dec 14 18:45:16 2008 +0100
+++ b/src/HOL/ex/LocaleTest2.thy	Sun Dec 14 18:45:51 2008 +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 -
@@ -837,7 +837,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 -
@@ -887,7 +887,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)" ..