diff -r c50fc8023ac0 -r a7f961fb62c6 src/HOL/Lattice/Lattice.thy
--- a/src/HOL/Lattice/Lattice.thy	Mon Oct 23 22:09:52 2000 +0200
+++ b/src/HOL/Lattice/Lattice.thy	Mon Oct 23 22:10:36 2000 +0200
@@ -109,7 +109,7 @@
 *}
 
 instance dual :: (lattice) lattice
-proof intro_classes
+proof
   fix x' y' :: "'a::lattice dual"
   show "\<exists>inf'. is_inf x' y' inf'"
   proof -
@@ -361,7 +361,7 @@
 qed
 
 instance linear_order < lattice
-proof intro_classes
+proof
   fix x y :: "'a::linear_order"
   from is_inf_minimum show "\<exists>inf. is_inf x y inf" ..
   from is_sup_maximum show "\<exists>sup. is_sup x y sup" ..
@@ -450,7 +450,7 @@
 qed
 
 instance * :: (lattice, lattice) lattice
-proof intro_classes
+proof
   fix p q :: "'a::lattice \<times> 'b::lattice"
   from is_inf_prod show "\<exists>inf. is_inf p q inf" ..
   from is_sup_prod show "\<exists>sup. is_sup p q sup" ..
@@ -520,7 +520,7 @@
 qed
 
 instance fun :: ("term", lattice) lattice
-proof intro_classes
+proof
   fix f g :: "'a \<Rightarrow> 'b::lattice"
   show "\<exists>inf. is_inf f g inf" by rule (rule is_inf_fun) (* FIXME @{text "from \<dots> show \<dots> .."} does not work!? unification incompleteness!? *)
   show "\<exists>sup. is_sup f g sup" by rule (rule is_sup_fun)