avoid explicit mandatory prefix markers when prefixes are mandatory implicitly
authorhaftmann
Mon Jul 12 11:39:27 2010 +0200 (2010-07-12)
changeset 37770cddb3106adb8
parent 37769 4511931c0692
child 37771 1bec64044b5e
avoid explicit mandatory prefix markers when prefixes are mandatory implicitly
src/HOL/Finite_Set.thy
src/HOL/GCD.thy
src/HOL/Library/Polynomial.thy
src/HOLCF/ConvexPD.thy
src/HOLCF/LowerPD.thy
src/HOLCF/Representable.thy
src/HOLCF/UpperPD.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Mon Jul 12 11:21:56 2010 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Mon Jul 12 11:39:27 2010 +0200
     1.3 @@ -1888,7 +1888,7 @@
     1.4  definition card :: "'a set \<Rightarrow> nat" where
     1.5    "card A = (if finite A then fold_image (op +) (\<lambda>x. 1) 0 A else 0)"
     1.6  
     1.7 -interpretation card!: folding_image_simple "op +" 0 "\<lambda>x. 1" card proof
     1.8 +interpretation card: folding_image_simple "op +" 0 "\<lambda>x. 1" card proof
     1.9  qed (simp add: card_def)
    1.10  
    1.11  lemma card_infinite [simp]:
     2.1 --- a/src/HOL/GCD.thy	Mon Jul 12 11:21:56 2010 +0200
     2.2 +++ b/src/HOL/GCD.thy	Mon Jul 12 11:39:27 2010 +0200
     2.3 @@ -302,11 +302,11 @@
     2.4  lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
     2.5    by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith)
     2.6  
     2.7 -interpretation gcd_nat!: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat"
     2.8 +interpretation gcd_nat: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat"
     2.9  proof
    2.10  qed (auto intro: dvd_antisym dvd_trans)
    2.11  
    2.12 -interpretation gcd_int!: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int"
    2.13 +interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int"
    2.14  proof
    2.15  qed (simp_all add: gcd_int_def gcd_nat.assoc gcd_nat.commute gcd_nat.left_commute)
    2.16  
    2.17 @@ -1383,7 +1383,7 @@
    2.18      (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
    2.19    by (auto intro: dvd_antisym [transferred] lcm_least_int)
    2.20  
    2.21 -interpretation lcm_nat!: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
    2.22 +interpretation lcm_nat: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
    2.23  proof
    2.24    fix n m p :: nat
    2.25    show "lcm (lcm n m) p = lcm n (lcm m p)"
    2.26 @@ -1392,7 +1392,7 @@
    2.27      by (simp add: lcm_nat_def gcd_commute_nat field_simps)
    2.28  qed
    2.29  
    2.30 -interpretation lcm_int!: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int"
    2.31 +interpretation lcm_int: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int"
    2.32  proof
    2.33    fix n m p :: int
    2.34    show "lcm (lcm n m) p = lcm n (lcm m p)"
     3.1 --- a/src/HOL/Library/Polynomial.thy	Mon Jul 12 11:21:56 2010 +0200
     3.2 +++ b/src/HOL/Library/Polynomial.thy	Mon Jul 12 11:39:27 2010 +0200
     3.3 @@ -1195,7 +1195,7 @@
     3.4      by (rule poly_dvd_antisym)
     3.5  qed
     3.6  
     3.7 -interpretation poly_gcd!: abel_semigroup poly_gcd
     3.8 +interpretation poly_gcd: abel_semigroup poly_gcd
     3.9  proof
    3.10    fix x y z :: "'a poly"
    3.11    show "poly_gcd (poly_gcd x y) z = poly_gcd x (poly_gcd y z)"
     4.1 --- a/src/HOLCF/ConvexPD.thy	Mon Jul 12 11:21:56 2010 +0200
     4.2 +++ b/src/HOLCF/ConvexPD.thy	Mon Jul 12 11:39:27 2010 +0200
     4.3 @@ -279,7 +279,7 @@
     4.4    "approx n\<cdot>(xs +\<natural> ys) = approx n\<cdot>xs +\<natural> approx n\<cdot>ys"
     4.5  by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
     4.6  
     4.7 -interpretation convex_add!: semilattice convex_add proof
     4.8 +interpretation convex_add: semilattice convex_add proof
     4.9    fix xs ys zs :: "'a convex_pd"
    4.10    show "(xs +\<natural> ys) +\<natural> zs = xs +\<natural> (ys +\<natural> zs)"
    4.11      apply (induct xs ys arbitrary: zs rule: convex_pd.principal_induct2, simp, simp)
     5.1 --- a/src/HOLCF/LowerPD.thy	Mon Jul 12 11:21:56 2010 +0200
     5.2 +++ b/src/HOLCF/LowerPD.thy	Mon Jul 12 11:39:27 2010 +0200
     5.3 @@ -234,7 +234,7 @@
     5.4    "approx n\<cdot>(xs +\<flat> ys) = (approx n\<cdot>xs) +\<flat> (approx n\<cdot>ys)"
     5.5  by (induct xs ys rule: lower_pd.principal_induct2, simp, simp, simp)
     5.6  
     5.7 -interpretation lower_add!: semilattice lower_add proof
     5.8 +interpretation lower_add: semilattice lower_add proof
     5.9    fix xs ys zs :: "'a lower_pd"
    5.10    show "(xs +\<flat> ys) +\<flat> zs = xs +\<flat> (ys +\<flat> zs)"
    5.11      apply (induct xs ys arbitrary: zs rule: lower_pd.principal_induct2, simp, simp)
     6.1 --- a/src/HOLCF/Representable.thy	Mon Jul 12 11:21:56 2010 +0200
     6.2 +++ b/src/HOLCF/Representable.thy	Mon Jul 12 11:39:27 2010 +0200
     6.3 @@ -21,7 +21,7 @@
     6.4    fixes prj :: "udom \<rightarrow> 'a::pcpo"
     6.5    assumes ep_pair_emb_prj: "ep_pair emb prj"
     6.6  
     6.7 -interpretation rep!:
     6.8 +interpretation rep:
     6.9    pcpo_ep_pair
    6.10      "emb :: 'a::rep \<rightarrow> udom"
    6.11      "prj :: udom \<rightarrow> 'a::rep"
     7.1 --- a/src/HOLCF/UpperPD.thy	Mon Jul 12 11:21:56 2010 +0200
     7.2 +++ b/src/HOLCF/UpperPD.thy	Mon Jul 12 11:39:27 2010 +0200
     7.3 @@ -232,7 +232,7 @@
     7.4    "approx n\<cdot>(xs +\<sharp> ys) = (approx n\<cdot>xs) +\<sharp> (approx n\<cdot>ys)"
     7.5  by (induct xs ys rule: upper_pd.principal_induct2, simp, simp, simp)
     7.6  
     7.7 -interpretation upper_add!: semilattice upper_add proof
     7.8 +interpretation upper_add: semilattice upper_add proof
     7.9    fix xs ys zs :: "'a upper_pd"
    7.10    show "(xs +\<sharp> ys) +\<sharp> zs = xs +\<sharp> (ys +\<sharp> zs)"
    7.11      apply (induct xs ys arbitrary: zs rule: upper_pd.principal_induct2, simp, simp)