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>"} *}