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