# HG changeset patch
# User haftmann
# Date 1278927567 -7200
# Node ID cddb3106adb898c18f173e17a3be1a818c63c3bf
# Parent  4511931c069266855950aafdeb8ec0bf14a7bbec
avoid explicit mandatory prefix markers when prefixes are mandatory implicitly

diff -r 4511931c0692 -r cddb3106adb8 src/HOL/Finite_Set.thy
--- 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]:
diff -r 4511931c0692 -r cddb3106adb8 src/HOL/GCD.thy
--- 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)"
diff -r 4511931c0692 -r cddb3106adb8 src/HOL/Library/Polynomial.thy
--- 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)"
diff -r 4511931c0692 -r cddb3106adb8 src/HOLCF/ConvexPD.thy
--- 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)
diff -r 4511931c0692 -r cddb3106adb8 src/HOLCF/LowerPD.thy
--- 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)
diff -r 4511931c0692 -r cddb3106adb8 src/HOLCF/Representable.thy
--- 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"
diff -r 4511931c0692 -r cddb3106adb8 src/HOLCF/UpperPD.thy
--- 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)