src/HOL/Algebra/IntRing.thy
changeset 44655 fe0365331566
parent 41433 1b8ff770f02c
child 44821 a92f65e174cf
     1.1 --- a/src/HOL/Algebra/IntRing.thy	Fri Sep 02 17:58:32 2011 +0200
     1.2 +++ b/src/HOL/Algebra/IntRing.thy	Fri Sep 02 18:17:45 2011 +0200
     1.3 @@ -62,7 +62,7 @@
     1.4      and "pow \<Z> x n = x^n"
     1.5  proof -
     1.6    -- "Specification"
     1.7 -  show "monoid \<Z>" proof qed auto
     1.8 +  show "monoid \<Z>" by default auto
     1.9    then interpret int: monoid \<Z> .
    1.10  
    1.11    -- "Carrier"
    1.12 @@ -79,7 +79,7 @@
    1.13    where "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
    1.14  proof -
    1.15    -- "Specification"
    1.16 -  show "comm_monoid \<Z>" proof qed auto
    1.17 +  show "comm_monoid \<Z>" by default auto
    1.18    then interpret int: comm_monoid \<Z> .
    1.19  
    1.20    -- "Operations"
    1.21 @@ -105,7 +105,7 @@
    1.22      and int_finsum_eq: "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
    1.23  proof -
    1.24    -- "Specification"
    1.25 -  show "abelian_monoid \<Z>" proof qed auto
    1.26 +  show "abelian_monoid \<Z>" by default auto
    1.27    then interpret int: abelian_monoid \<Z> .
    1.28  
    1.29    -- "Carrier"
    1.30 @@ -189,7 +189,7 @@
    1.31      and "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
    1.32  proof -
    1.33    show "partial_order (| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
    1.34 -    proof qed simp_all
    1.35 +    by default simp_all
    1.36    show "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
    1.37      by simp
    1.38    show "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
    1.39 @@ -226,7 +226,7 @@
    1.40  
    1.41  interpretation int (* [unfolded UNIV] *) :
    1.42    total_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
    1.43 -  proof qed clarsimp
    1.44 +  by default clarsimp
    1.45  
    1.46  
    1.47  subsection {* Generated Ideals of @{text "\<Z>"} *}