--- a/src/HOL/Lattice/Lattice.thy Sun Feb 11 20:38:40 2001 +0100
+++ b/src/HOL/Lattice/Lattice.thy Mon Feb 12 20:43:12 2001 +0100
@@ -15,7 +15,7 @@
as well).
*}
-axclass lattice < partial_order
+axclass lattice \<subseteq> partial_order
ex_inf: "\<exists>inf. is_inf x y inf"
ex_sup: "\<exists>sup. is_sup x y sup"
@@ -360,7 +360,7 @@
with leq_linear show "?max \<sqsubseteq> z" by (auto simp add: maximum_def)
qed
-instance linear_order < lattice
+instance linear_order \<subseteq> lattice
proof
fix x y :: "'a::linear_order"
from is_inf_minimum show "\<exists>inf. is_inf x y inf" ..