# HG changeset patch
# User paulson
# Date 833794860 -7200
# Node ID ab45b881fa62c85dacc26249e5d6780e97a8e39e
# Parent  cc5f55a0fbd71d804bc9a0cb5ce40d64eb397fe8
Shortened a proof

diff -r cc5f55a0fbd7 -r ab45b881fa62 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Fri May 31 20:25:59 1996 +0200
+++ b/src/HOL/Finite.ML	Mon Jun 03 11:41:00 1996 +0200
@@ -201,9 +201,7 @@
 by (etac exE 1);
 by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
 by (rtac exI 1);
-by (rtac conjI 1);
- br disjI2 1;
- br refl 1;
+by (rtac (refl RS disjI2 RS conjI) 1);
 by (etac equalityE 1);
 by (asm_full_simp_tac
      (!simpset addsimps [subset_insert,Collect_conv_insert, less_Suc_eq]) 1);
diff -r cc5f55a0fbd7 -r ab45b881fa62 src/ZF/Perm.ML
--- a/src/ZF/Perm.ML	Fri May 31 20:25:59 1996 +0200
+++ b/src/ZF/Perm.ML	Mon Jun 03 11:41:00 1996 +0200
@@ -542,13 +542,7 @@
 by (fast_tac ZF_cs 1);
 by (cut_facts_tac [major] 1);
 by (rewtac inj_def);
-by (safe_tac ZF_cs);
-by (etac range_type 1);
-by (assume_tac 1);
-by (dtac apply_equality 1);
-by (assume_tac 1);
-by (res_inst_tac [("a","m")] mem_irrefl 1);
-by (fast_tac ZF_cs 1);
+by (fast_tac (ZF_cs addEs [range_type, mem_irrefl] addDs [apply_equality]) 1);
 qed "inj_succ_restrict";
 
 goalw Perm.thy [inj_def]
diff -r cc5f55a0fbd7 -r ab45b881fa62 src/ZF/ex/misc.ML
--- a/src/ZF/ex/misc.ML	Fri May 31 20:25:59 1996 +0200
+++ b/src/ZF/ex/misc.ML	Mon Jun 03 11:41:00 1996 +0200
@@ -60,10 +60,7 @@
 
 goalw ZF.thy [Pi_def, function_def]
     "r: domain(r)->B  <->  r <= domain(r)*B & (ALL X. r `` (r -`` X) <= X)";
-by (safe_tac ZF_cs);
-by (fast_tac ZF_cs 1);
-by (eres_inst_tac [("x", "{y}")] allE 1);
-by (fast_tac ZF_cs 1);
+by (best_tac ZF_cs 1);
 result();