tuned;

--- a/src/HOL/AxClasses/Lattice/Lattice.ML	Wed Oct 21 16:06:09 1998 +0200
+++ b/src/HOL/AxClasses/Lattice/Lattice.ML	Wed Oct 21 16:34:18 1998 +0200
@@ -1,3 +1,12 @@
+
+context HOL.thy;
+
+Goalw [Ex_def] "EX x. P x ==> P (@x. P x)";
+  ba 1;
+qed "selectI1";
+
+context thy;
+
 
 
 (** basic properties of "&&" and "||" **)

--- a/src/HOL/AxClasses/Lattice/OrdDefs.ML	Wed Oct 21 16:06:09 1998 +0200
+++ b/src/HOL/AxClasses/Lattice/OrdDefs.ML	Wed Oct 21 16:34:18 1998 +0200
@@ -66,8 +66,9 @@
 qed "le_dual_refl";
 
 Goalw [le_dual_def] "x [= y & y [= z --> x [= (z::'a::quasi_order dual)";
-  by (stac conj_commut 1);
-  by (rtac le_trans 1);
+  br impI 1;
+  br (le_trans RS mp) 1;
+  by (Blast_tac 1);
 qed "le_dual_trans";
 
 Goalw [le_dual_def] "x [= y & y [= x --> x = (y::'a::partial_order dual)";

--- a/src/HOL/AxClasses/Lattice/ROOT.ML	Wed Oct 21 16:06:09 1998 +0200
+++ b/src/HOL/AxClasses/Lattice/ROOT.ML	Wed Oct 21 16:34:18 1998 +0200
@@ -12,8 +12,6 @@
 set show_types;
 set show_sorts;
 
-use "tools.ML";
-
 use_thy "Order";
 use_thy "OrdDefs";
 use_thy "OrdInsts";

--- a/src/HOL/AxClasses/Lattice/tools.ML	Wed Oct 21 16:06:09 1998 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-
-(** generic tools **)
-
-val prems = goalw HOL.thy [Ex_def] "EX x. P x ==> P (@x. P x)";
-  by (resolve_tac prems 1);
-qed "selectI1";
-
-goal HOL.thy "(P & Q) = (Q & P)";
-  by (Fast_tac 1);
-qed "conj_commut";

--- a/src/HOL/IsaMakefile	Wed Oct 21 16:06:09 1998 +0200
+++ b/src/HOL/IsaMakefile	Wed Oct 21 16:34:18 1998 +0200
@@ -259,7 +259,7 @@
   AxClasses/Lattice/Lattice.thy AxClasses/Lattice/OrdDefs.ML \
   AxClasses/Lattice/OrdDefs.thy AxClasses/Lattice/OrdInsts.thy \
   AxClasses/Lattice/Order.ML AxClasses/Lattice/Order.thy \
-  AxClasses/Lattice/ROOT.ML AxClasses/Lattice/tools.ML
+  AxClasses/Lattice/ROOT.ML
 	@$(ISATOOL) usedir -s AxClasses-Lattice $(OUT)/HOL AxClasses/Lattice