src/HOL/Algebra/IntRing.thy
changeset 28085 914183e229e9
parent 27717 21bbd410ba04
child 28524 644b62cf678f
     1.1 --- a/src/HOL/Algebra/IntRing.thy	Tue Sep 02 16:55:33 2008 +0200
     1.2 +++ b/src/HOL/Algebra/IntRing.thy	Tue Sep 02 17:31:20 2008 +0200
     1.3 @@ -204,7 +204,7 @@
     1.4    "(True ==> PROP R) == PROP R"
     1.5    by simp_all
     1.6  
     1.7 -interpretation int [unfolded UNIV]:
     1.8 +interpretation int (* FIXME [unfolded UNIV] *) :
     1.9    partial_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
    1.10    where "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
    1.11      and "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
    1.12 @@ -220,7 +220,7 @@
    1.13      by (simp add: lless_def) auto
    1.14  qed
    1.15  
    1.16 -interpretation int [unfolded UNIV]:
    1.17 +interpretation int (* FIXME [unfolded UNIV] *) :
    1.18    lattice ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
    1.19    where "join (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = max x y"
    1.20      and "meet (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = min x y"
    1.21 @@ -246,7 +246,7 @@
    1.22      done
    1.23  qed
    1.24  
    1.25 -interpretation int [unfolded UNIV]:
    1.26 +interpretation int (* [unfolded UNIV] *) :
    1.27    total_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
    1.28    by unfold_locales clarsimp
    1.29