src/HOL/Algebra/IntRing.thy
 changeset 55926 3ef14caf5637 parent 55242 413ec965f95d child 55991 3fa6e6c81788
```     1.1 --- a/src/HOL/Algebra/IntRing.thy	Wed Mar 05 20:07:43 2014 +0100
1.2 +++ b/src/HOL/Algebra/IntRing.thy	Wed Mar 05 21:51:30 2014 +0100
1.3 @@ -23,7 +23,7 @@
1.4
1.5  abbreviation
1.6    int_ring :: "int ring" ("\<Z>") where
1.7 -  "int_ring == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
1.8 +  "int_ring == \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
1.9
1.10  lemma int_Zcarr [intro!, simp]:
1.11    "k \<in> carrier \<Z>"
1.12 @@ -183,27 +183,27 @@
1.13    by simp_all
1.14
1.15  interpretation int (* FIXME [unfolded UNIV] *) :
1.16 -  partial_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
1.17 -  where "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
1.18 -    and "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
1.19 -    and "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
1.20 +  partial_order "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
1.21 +  where "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> = UNIV"
1.22 +    and "le \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x \<le> y)"
1.23 +    and "lless \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x < y)"
1.24  proof -
1.25 -  show "partial_order (| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
1.26 +  show "partial_order \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
1.27      by default simp_all
1.28 -  show "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
1.29 +  show "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> = UNIV"
1.30      by simp
1.31 -  show "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
1.32 +  show "le \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x \<le> y)"
1.33      by simp
1.34 -  show "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
1.35 +  show "lless \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x < y)"
1.36      by (simp add: lless_def) auto
1.37  qed
1.38
1.39  interpretation int (* FIXME [unfolded UNIV] *) :
1.40 -  lattice "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
1.41 -  where "join (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = max x y"
1.42 -    and "meet (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = min x y"
1.43 +  lattice "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
1.44 +  where "join \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = max x y"
1.45 +    and "meet \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = min x y"
1.46  proof -
1.47 -  let ?Z = "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
1.48 +  let ?Z = "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
1.49    show "lattice ?Z"
1.50      apply unfold_locales
1.51      apply (simp add: least_def Upper_def)
1.52 @@ -225,7 +225,7 @@
1.53  qed
1.54
1.55  interpretation int (* [unfolded UNIV] *) :
1.56 -  total_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
1.57 +  total_order "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
1.58    by default clarsimp
1.59
1.60
```