diff -r a05ca48ef263 -r 914183e229e9 src/HOL/Algebra/IntRing.thy --- 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 \ |)"] where "carrier (| carrier = UNIV::int set, eq = op =, le = op \ |) = UNIV" and "le (| carrier = UNIV::int set, eq = op =, le = op \ |) x y = (x \ 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 \ |)"] where "join (| carrier = UNIV::int set, eq = op =, le = op \ |) x y = max x y" and "meet (| carrier = UNIV::int set, eq = op =, le = op \ |) 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 \ |)"] by unfold_locales clarsimp