src/HOL/Algebra/IntRing.thy
 changeset 67396 172a02125bfa parent 67344 9a0bb8e2be07 child 67399 eab6ce8368fa
```     1.1 --- a/src/HOL/Algebra/IntRing.thy	Tue Jan 09 20:15:36 2018 +0100
1.2 +++ b/src/HOL/Algebra/IntRing.thy	Wed Jan 10 12:35:03 2018 +0100
1.3 @@ -172,27 +172,27 @@
1.4    by simp_all
1.5
1.6  interpretation int (* FIXME [unfolded UNIV] *) :
1.7 -  partial_order "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
1.8 -  rewrites "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> = UNIV"
1.9 -    and "le \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x \<le> y)"
1.10 -    and "lless \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x < y)"
1.11 +  partial_order "\<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr>"
1.12 +  rewrites "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> = UNIV"
1.13 +    and "le \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> x y = (x \<le> y)"
1.14 +    and "lless \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> x y = (x < y)"
1.15  proof -
1.16 -  show "partial_order \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
1.17 +  show "partial_order \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr>"
1.18      by standard simp_all
1.19 -  show "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> = UNIV"
1.20 +  show "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> = UNIV"
1.21      by simp
1.22 -  show "le \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x \<le> y)"
1.23 +  show "le \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> x y = (x \<le> y)"
1.24      by simp
1.25 -  show "lless \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x < y)"
1.26 +  show "lless \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> x y = (x < y)"
1.27      by (simp add: lless_def) auto
1.28  qed
1.29
1.30  interpretation int (* FIXME [unfolded UNIV] *) :
1.31 -  lattice "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
1.32 -  rewrites "join \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = max x y"
1.33 -    and "meet \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = min x y"
1.34 +  lattice "\<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr>"
1.35 +  rewrites "join \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> x y = max x y"
1.36 +    and "meet \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> x y = min x y"
1.37  proof -
1.38 -  let ?Z = "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
1.39 +  let ?Z = "\<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr>"
1.40    show "lattice ?Z"
1.41      apply unfold_locales
1.42      apply (simp add: least_def Upper_def)
1.43 @@ -214,7 +214,7 @@
1.44  qed
1.45
1.46  interpretation int (* [unfolded UNIV] *) :
1.47 -  total_order "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
1.48 +  total_order "\<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr>"
1.49    by standard clarsimp
1.50
1.51
```