--- a/src/HOL/Finite_Set.thy Mon Jul 12 11:21:56 2010 +0200
+++ b/src/HOL/Finite_Set.thy Mon Jul 12 11:39:27 2010 +0200
@@ -1888,7 +1888,7 @@
definition card :: "'a set \<Rightarrow> nat" where
"card A = (if finite A then fold_image (op +) (\<lambda>x. 1) 0 A else 0)"
-interpretation card!: folding_image_simple "op +" 0 "\<lambda>x. 1" card proof
+interpretation card: folding_image_simple "op +" 0 "\<lambda>x. 1" card proof
qed (simp add: card_def)
lemma card_infinite [simp]:
--- a/src/HOL/GCD.thy Mon Jul 12 11:21:56 2010 +0200
+++ b/src/HOL/GCD.thy Mon Jul 12 11:39:27 2010 +0200
@@ -302,11 +302,11 @@
lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith)
-interpretation gcd_nat!: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat"
+interpretation gcd_nat: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat"
proof
qed (auto intro: dvd_antisym dvd_trans)
-interpretation gcd_int!: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int"
+interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int"
proof
qed (simp_all add: gcd_int_def gcd_nat.assoc gcd_nat.commute gcd_nat.left_commute)
@@ -1383,7 +1383,7 @@
(\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
by (auto intro: dvd_antisym [transferred] lcm_least_int)
-interpretation lcm_nat!: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
+interpretation lcm_nat: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
proof
fix n m p :: nat
show "lcm (lcm n m) p = lcm n (lcm m p)"
@@ -1392,7 +1392,7 @@
by (simp add: lcm_nat_def gcd_commute_nat field_simps)
qed
-interpretation lcm_int!: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int"
+interpretation lcm_int: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int"
proof
fix n m p :: int
show "lcm (lcm n m) p = lcm n (lcm m p)"
--- a/src/HOL/Library/Polynomial.thy Mon Jul 12 11:21:56 2010 +0200
+++ b/src/HOL/Library/Polynomial.thy Mon Jul 12 11:39:27 2010 +0200
@@ -1195,7 +1195,7 @@
by (rule poly_dvd_antisym)
qed
-interpretation poly_gcd!: abel_semigroup poly_gcd
+interpretation poly_gcd: abel_semigroup poly_gcd
proof
fix x y z :: "'a poly"
show "poly_gcd (poly_gcd x y) z = poly_gcd x (poly_gcd y z)"
--- a/src/HOLCF/ConvexPD.thy Mon Jul 12 11:21:56 2010 +0200
+++ b/src/HOLCF/ConvexPD.thy Mon Jul 12 11:39:27 2010 +0200
@@ -279,7 +279,7 @@
"approx n\<cdot>(xs +\<natural> ys) = approx n\<cdot>xs +\<natural> approx n\<cdot>ys"
by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
-interpretation convex_add!: semilattice convex_add proof
+interpretation convex_add: semilattice convex_add proof
fix xs ys zs :: "'a convex_pd"
show "(xs +\<natural> ys) +\<natural> zs = xs +\<natural> (ys +\<natural> zs)"
apply (induct xs ys arbitrary: zs rule: convex_pd.principal_induct2, simp, simp)
--- a/src/HOLCF/LowerPD.thy Mon Jul 12 11:21:56 2010 +0200
+++ b/src/HOLCF/LowerPD.thy Mon Jul 12 11:39:27 2010 +0200
@@ -234,7 +234,7 @@
"approx n\<cdot>(xs +\<flat> ys) = (approx n\<cdot>xs) +\<flat> (approx n\<cdot>ys)"
by (induct xs ys rule: lower_pd.principal_induct2, simp, simp, simp)
-interpretation lower_add!: semilattice lower_add proof
+interpretation lower_add: semilattice lower_add proof
fix xs ys zs :: "'a lower_pd"
show "(xs +\<flat> ys) +\<flat> zs = xs +\<flat> (ys +\<flat> zs)"
apply (induct xs ys arbitrary: zs rule: lower_pd.principal_induct2, simp, simp)
--- a/src/HOLCF/Representable.thy Mon Jul 12 11:21:56 2010 +0200
+++ b/src/HOLCF/Representable.thy Mon Jul 12 11:39:27 2010 +0200
@@ -21,7 +21,7 @@
fixes prj :: "udom \<rightarrow> 'a::pcpo"
assumes ep_pair_emb_prj: "ep_pair emb prj"
-interpretation rep!:
+interpretation rep:
pcpo_ep_pair
"emb :: 'a::rep \<rightarrow> udom"
"prj :: udom \<rightarrow> 'a::rep"
--- a/src/HOLCF/UpperPD.thy Mon Jul 12 11:21:56 2010 +0200
+++ b/src/HOLCF/UpperPD.thy Mon Jul 12 11:39:27 2010 +0200
@@ -232,7 +232,7 @@
"approx n\<cdot>(xs +\<sharp> ys) = (approx n\<cdot>xs) +\<sharp> (approx n\<cdot>ys)"
by (induct xs ys rule: upper_pd.principal_induct2, simp, simp, simp)
-interpretation upper_add!: semilattice upper_add proof
+interpretation upper_add: semilattice upper_add proof
fix xs ys zs :: "'a upper_pd"
show "(xs +\<sharp> ys) +\<sharp> zs = xs +\<sharp> (ys +\<sharp> zs)"
apply (induct xs ys arbitrary: zs rule: upper_pd.principal_induct2, simp, simp)