# HG changeset patch
# User paulson
# Date 880635531 -3600
# Node ID e220fb9bd4e53107f2fc64a589a9216dbb1fe53b
# Parent  cad4f24be60b9dac64222707097d7a3d4ae5a713
Deleted some needless addSIs; got rid of a slow Blast_tac

diff -r cad4f24be60b -r e220fb9bd4e5 src/ZF/Order.ML
--- a/src/ZF/Order.ML	Thu Nov 27 13:38:06 1997 +0100
+++ b/src/ZF/Order.ML	Thu Nov 27 13:58:51 1997 +0100
@@ -140,7 +140,7 @@
 qed "tot_ord_Int_iff";
 
 goalw Order.thy [wf_on_def, wf_def] "wf[A](r Int A*A) <-> wf[A](r)";
-by (Blast_tac 1);
+by (Fast_tac 1);   (*10 times faster than Blast_tac!*) 
 qed "wf_on_Int_iff";
 
 goalw Order.thy [well_ord_def] "well_ord(A,r Int A*A) <-> well_ord(A,r)";
@@ -591,12 +591,12 @@
 
 goalw Order.thy [irrefl_def] 
             "!!A. irrefl(A,r) ==> irrefl(A,converse(r))";
-by (blast_tac (claset() addSIs [converseI]) 1);
+by (Blast_tac 1);
 qed "irrefl_converse";
 
 goalw Order.thy [trans_on_def] 
     "!!A. trans[A](r) ==> trans[A](converse(r))";
-by (blast_tac (claset() addSIs [converseI]) 1);
+by (Blast_tac 1);
 qed "trans_on_converse";
 
 goalw Order.thy [part_ord_def] 
@@ -606,7 +606,7 @@
 
 goalw Order.thy [linear_def] 
     "!!A. linear(A,r) ==> linear(A,converse(r))";
-by (blast_tac (claset() addSIs [converseI]) 1);
+by (Blast_tac 1);
 qed "linear_converse";
 
 goalw Order.thy [tot_ord_def]