--- 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)" ..