Shortened a proof
authorpaulson
Mon Jun 03 11:41:00 1996 +0200 (1996-06-03)
changeset 1782ab45b881fa62
parent 1781 cc5f55a0fbd7
child 1783 173ce86b4c22
Shortened a proof
src/HOL/Finite.ML
src/ZF/Perm.ML
src/ZF/ex/misc.ML
     1.1 --- a/src/HOL/Finite.ML	Fri May 31 20:25:59 1996 +0200
     1.2 +++ b/src/HOL/Finite.ML	Mon Jun 03 11:41:00 1996 +0200
     1.3 @@ -201,9 +201,7 @@
     1.4  by (etac exE 1);
     1.5  by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
     1.6  by (rtac exI 1);
     1.7 -by (rtac conjI 1);
     1.8 - br disjI2 1;
     1.9 - br refl 1;
    1.10 +by (rtac (refl RS disjI2 RS conjI) 1);
    1.11  by (etac equalityE 1);
    1.12  by (asm_full_simp_tac
    1.13       (!simpset addsimps [subset_insert,Collect_conv_insert, less_Suc_eq]) 1);
     2.1 --- a/src/ZF/Perm.ML	Fri May 31 20:25:59 1996 +0200
     2.2 +++ b/src/ZF/Perm.ML	Mon Jun 03 11:41:00 1996 +0200
     2.3 @@ -542,13 +542,7 @@
     2.4  by (fast_tac ZF_cs 1);
     2.5  by (cut_facts_tac [major] 1);
     2.6  by (rewtac inj_def);
     2.7 -by (safe_tac ZF_cs);
     2.8 -by (etac range_type 1);
     2.9 -by (assume_tac 1);
    2.10 -by (dtac apply_equality 1);
    2.11 -by (assume_tac 1);
    2.12 -by (res_inst_tac [("a","m")] mem_irrefl 1);
    2.13 -by (fast_tac ZF_cs 1);
    2.14 +by (fast_tac (ZF_cs addEs [range_type, mem_irrefl] addDs [apply_equality]) 1);
    2.15  qed "inj_succ_restrict";
    2.16  
    2.17  goalw Perm.thy [inj_def]
     3.1 --- a/src/ZF/ex/misc.ML	Fri May 31 20:25:59 1996 +0200
     3.2 +++ b/src/ZF/ex/misc.ML	Mon Jun 03 11:41:00 1996 +0200
     3.3 @@ -60,10 +60,7 @@
     3.4  
     3.5  goalw ZF.thy [Pi_def, function_def]
     3.6      "r: domain(r)->B  <->  r <= domain(r)*B & (ALL X. r `` (r -`` X) <= X)";
     3.7 -by (safe_tac ZF_cs);
     3.8 -by (fast_tac ZF_cs 1);
     3.9 -by (eres_inst_tac [("x", "{y}")] allE 1);
    3.10 -by (fast_tac ZF_cs 1);
    3.11 +by (best_tac ZF_cs 1);
    3.12  result();
    3.13  
    3.14