src/HOL/Algebra/IntRing.thy
changeset 28085 914183e229e9
parent 27717 21bbd410ba04
child 28524 644b62cf678f
--- a/src/HOL/Algebra/IntRing.thy	Tue Sep 02 16:55:33 2008 +0200
+++ b/src/HOL/Algebra/IntRing.thy	Tue Sep 02 17:31:20 2008 +0200
@@ -204,7 +204,7 @@
   "(True ==> PROP R) == PROP R"
   by simp_all
 
-interpretation int [unfolded UNIV]:
+interpretation int (* FIXME [unfolded UNIV] *) :
   partial_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
   where "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
     and "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
@@ -220,7 +220,7 @@
     by (simp add: lless_def) auto
 qed
 
-interpretation int [unfolded UNIV]:
+interpretation int (* FIXME [unfolded UNIV] *) :
   lattice ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
   where "join (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = max x y"
     and "meet (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = min x y"
@@ -246,7 +246,7 @@
     done
 qed
 
-interpretation int [unfolded UNIV]:
+interpretation int (* [unfolded UNIV] *) :
   total_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
   by unfold_locales clarsimp