src/HOL/Algebra/IntRing.thy
 changeset 28823 dcbef866c9e2 parent 28524 644b62cf678f child 29237 e90d9d51106b
```     1.1 --- a/src/HOL/Algebra/IntRing.thy	Mon Nov 17 17:00:27 2008 +0100
1.2 +++ b/src/HOL/Algebra/IntRing.thy	Mon Nov 17 17:00:55 2008 +0100
1.3 @@ -5,7 +5,7 @@
1.4  *)
1.5
1.6  theory IntRing
1.7 -imports QuotRing Int Primes
1.8 +imports QuotRing Lattice Int Primes
1.9  begin
1.10
1.11
1.12 @@ -104,7 +104,7 @@
1.13      and "pow \<Z> x n = x^n"
1.14  proof -
1.15    -- "Specification"
1.16 -  show "monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
1.17 +  show "monoid \<Z>" proof qed (auto simp: int_ring_def)
1.18    then interpret int: monoid ["\<Z>"] .
1.19
1.20    -- "Carrier"
1.21 @@ -121,7 +121,7 @@
1.22    where "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
1.23  proof -
1.24    -- "Specification"
1.25 -  show "comm_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
1.26 +  show "comm_monoid \<Z>" proof qed (auto simp: int_ring_def)
1.27    then interpret int: comm_monoid ["\<Z>"] .
1.28
1.29    -- "Operations"
1.30 @@ -146,7 +146,7 @@
1.31      and "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
1.32  proof -
1.33    -- "Specification"
1.34 -  show "abelian_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
1.35 +  show "abelian_monoid \<Z>" proof qed (auto simp: int_ring_def)
1.36    then interpret int: abelian_monoid ["\<Z>"] .
1.37
1.38    -- "Operations"
1.39 @@ -189,7 +189,7 @@
1.40  qed
1.41
1.42  interpretation int: "domain" ["\<Z>"]
1.43 -  by (unfold_locales) (auto simp: int_ring_def left_distrib right_distrib)
1.44 +  proof qed (auto simp: int_ring_def left_distrib right_distrib)
1.45
1.46
1.47  text {* Removal of occurrences of @{term UNIV} in interpretation result
1.48 @@ -211,7 +211,7 @@
1.49      and "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
1.50  proof -
1.51    show "partial_order (| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
1.52 -    by unfold_locales simp_all
1.53 +    proof qed simp_all
1.54    show "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
1.55      by simp
1.56    show "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
1.57 @@ -248,7 +248,7 @@
1.58
1.59  interpretation int (* [unfolded UNIV] *) :
1.60    total_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
1.61 -  by unfold_locales clarsimp
1.62 +  proof qed clarsimp
1.63
1.64
1.65  subsection {* Generated Ideals of @{text "\<Z>"} *}
```