expandshort
authorpaulson
Wed Mar 03 11:15:18 1999 +0100 (1999-03-03)
changeset 630108245f5a436d
parent 6300 3815b5b095cb
child 6302 957d8e203be1
expandshort
src/HOL/Arith.ML
src/HOL/Fun.ML
src/HOL/Induct/Acc.ML
src/HOL/Induct/Multiset0.ML
src/HOL/Integ/Bin.ML
src/HOL/Lambda/Eta.ML
src/HOL/Lambda/ListApplication.ML
src/HOL/Lex/NA.ML
src/HOL/Map.ML
src/HOL/Nat.ML
src/HOL/Ord.ML
src/HOL/Set.ML
src/HOL/TLA/Action.ML
src/HOL/equalities.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/Arith.ML	Wed Mar 03 11:12:29 1999 +0100
     1.2 +++ b/src/HOL/Arith.ML	Wed Mar 03 11:15:18 1999 +0100
     1.3 @@ -105,13 +105,13 @@
     1.4  AddIffs [zero_is_add];
     1.5  
     1.6  Goal "(m+n=1) = (m=1 & n=0 | m=0 & n=1)";
     1.7 -by(exhaust_tac "m" 1);
     1.8 -by(Auto_tac);
     1.9 +by (exhaust_tac "m" 1);
    1.10 +by (Auto_tac);
    1.11  qed "add_is_1";
    1.12  
    1.13  Goal "(1=m+n) = (m=1 & n=0 | m=0 & n=1)";
    1.14 -by(exhaust_tac "m" 1);
    1.15 -by(Auto_tac);
    1.16 +by (exhaust_tac "m" 1);
    1.17 +by (Auto_tac);
    1.18  qed "one_is_add";
    1.19  
    1.20  Goal "(0<m+n) = (0<m | 0<n)";
    1.21 @@ -185,7 +185,7 @@
    1.22  Goal "i+j < (k::nat) --> i<k";
    1.23  by (induct_tac "j" 1);
    1.24  by (ALLGOALS Asm_simp_tac);
    1.25 -by(blast_tac (claset() addDs [Suc_lessD]) 1);
    1.26 +by (blast_tac (claset() addDs [Suc_lessD]) 1);
    1.27  qed_spec_mp "add_lessD1";
    1.28  
    1.29  Goal "~ (i+j < (i::nat))";
    1.30 @@ -972,10 +972,10 @@
    1.31  
    1.32  (* Elimination of `-' on nat due to John Harrison *)
    1.33  Goal "P(a - b::nat) = (!d. (b = a + d --> P 0) & (a = b + d --> P d))";
    1.34 -by(case_tac "a <= b" 1);
    1.35 -by(Auto_tac);
    1.36 -by(eres_inst_tac [("x","b-a")] allE 1);
    1.37 -by(Auto_tac);
    1.38 +by (case_tac "a <= b" 1);
    1.39 +by (Auto_tac);
    1.40 +by (eres_inst_tac [("x","b-a")] allE 1);
    1.41 +by (Auto_tac);
    1.42  qed "nat_diff_split";
    1.43  
    1.44  (* FIXME: K true should be replaced by a sensible test to speed things up
    1.45 @@ -995,75 +995,75 @@
    1.46  (*** Subtraction laws -- mostly from Clemens Ballarin ***)
    1.47  
    1.48  Goal "[| a < (b::nat); c <= a |] ==> a-c < b-c";
    1.49 -by(arith_tac 1);
    1.50 +by (arith_tac 1);
    1.51  qed "diff_less_mono";
    1.52  
    1.53  Goal "a+b < (c::nat) ==> a < c-b";
    1.54 -by(arith_tac 1);
    1.55 +by (arith_tac 1);
    1.56  qed "add_less_imp_less_diff";
    1.57  
    1.58  Goal "(i < j-k) = (i+k < (j::nat))";
    1.59 -by(arith_tac 1);
    1.60 +by (arith_tac 1);
    1.61  qed "less_diff_conv";
    1.62  
    1.63  Goal "(j-k <= (i::nat)) = (j <= i+k)";
    1.64 -by(arith_tac 1);
    1.65 +by (arith_tac 1);
    1.66  qed "le_diff_conv";
    1.67  
    1.68  Goal "k <= j ==> (i <= j-k) = (i+k <= (j::nat))";
    1.69 -by(arith_tac 1);
    1.70 +by (arith_tac 1);
    1.71  qed "le_diff_conv2";
    1.72  
    1.73  Goal "Suc i <= n ==> Suc (n - Suc i) = n - i";
    1.74 -by(arith_tac 1);
    1.75 +by (arith_tac 1);
    1.76  qed "Suc_diff_Suc";
    1.77  
    1.78  Goal "i <= (n::nat) ==> n - (n - i) = i";
    1.79 -by(arith_tac 1);
    1.80 +by (arith_tac 1);
    1.81  qed "diff_diff_cancel";
    1.82  Addsimps [diff_diff_cancel];
    1.83  
    1.84  Goal "k <= (n::nat) ==> m <= n + m - k";
    1.85 -by(arith_tac 1);
    1.86 +by (arith_tac 1);
    1.87  qed "le_add_diff";
    1.88  
    1.89  Goal "[| 0<k; j<i |] ==> j+k-i < k";
    1.90 -by(arith_tac 1);
    1.91 +by (arith_tac 1);
    1.92  qed "add_diff_less";
    1.93  
    1.94  Goal "m-1 < n ==> m <= n";
    1.95 -by(arith_tac 1);
    1.96 +by (arith_tac 1);
    1.97  qed "pred_less_imp_le";
    1.98  
    1.99  Goal "j<=i ==> i - j < Suc i - j";
   1.100 -by(arith_tac 1);
   1.101 +by (arith_tac 1);
   1.102  qed "diff_less_Suc_diff";
   1.103  
   1.104  Goal "i - j <= Suc i - j";
   1.105 -by(arith_tac 1);
   1.106 +by (arith_tac 1);
   1.107  qed "diff_le_Suc_diff";
   1.108  AddIffs [diff_le_Suc_diff];
   1.109  
   1.110  Goal "n - Suc i <= n - i";
   1.111 -by(arith_tac 1);
   1.112 +by (arith_tac 1);
   1.113  qed "diff_Suc_le_diff";
   1.114  AddIffs [diff_Suc_le_diff];
   1.115  
   1.116  Goal "0 < n ==> (m <= n-1) = (m<n)";
   1.117 -by(arith_tac 1);
   1.118 +by (arith_tac 1);
   1.119  qed "le_pred_eq";
   1.120  
   1.121  Goal "0 < n ==> (m-1 < n) = (m<=n)";
   1.122 -by(arith_tac 1);
   1.123 +by (arith_tac 1);
   1.124  qed "less_pred_eq";
   1.125  
   1.126  (*In ordinary notation: if 0<n and n<=m then m-n < m *)
   1.127  Goal "[| 0<n; ~ m<n |] ==> m - n < m";
   1.128 -by(arith_tac 1);
   1.129 +by (arith_tac 1);
   1.130  qed "diff_less";
   1.131  
   1.132  Goal "[| 0<n; n<=m |] ==> m - n < m";
   1.133 -by(arith_tac 1);
   1.134 +by (arith_tac 1);
   1.135  qed "le_diff_less";
   1.136  
   1.137  
   1.138 @@ -1072,19 +1072,19 @@
   1.139  
   1.140  (* Monotonicity of subtraction in first argument *)
   1.141  Goal "m <= (n::nat) ==> (m-l) <= (n-l)";
   1.142 -by(arith_tac 1);
   1.143 +by (arith_tac 1);
   1.144  qed "diff_le_mono";
   1.145  
   1.146  Goal "m <= (n::nat) ==> (l-n) <= (l-m)";
   1.147 -by(arith_tac 1);
   1.148 +by (arith_tac 1);
   1.149  qed "diff_le_mono2";
   1.150  
   1.151  
   1.152  (*This proof requires natdiff_cancel_sums*)
   1.153  Goal "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)";
   1.154 -by(arith_tac 1);
   1.155 +by (arith_tac 1);
   1.156  qed "diff_less_mono2";
   1.157  
   1.158  Goal "[| m-n = 0; n-m = 0 |] ==>  m=n";
   1.159 -by(arith_tac 1);
   1.160 +by (arith_tac 1);
   1.161  qed "diffs0_imp_equal";
     2.1 --- a/src/HOL/Fun.ML	Wed Mar 03 11:12:29 1999 +0100
     2.2 +++ b/src/HOL/Fun.ML	Wed Mar 03 11:15:18 1999 +0100
     2.3 @@ -213,6 +213,14 @@
     2.4  by Auto_tac;
     2.5  qed "inv_image_comp";
     2.6  
     2.7 +Goal "inj f ==> (f a : f``A) = (a : A)";
     2.8 +by (blast_tac (claset() addDs [injD]) 1);
     2.9 +qed "inj_image_mem_iff";
    2.10 +
    2.11 +Goal "inj f ==> (f``A = f``B) = (A = B)";
    2.12 +by (blast_tac (claset() addSEs [equalityE] addDs [injD]) 1);
    2.13 +qed "inj_image_eq_iff";
    2.14 +
    2.15  val set_cs = claset() delrules [equalityI];
    2.16  
    2.17  
     3.1 --- a/src/HOL/Induct/Acc.ML	Wed Mar 03 11:12:29 1999 +0100
     3.2 +++ b/src/HOL/Induct/Acc.ML	Wed Mar 03 11:15:18 1999 +0100
     3.3 @@ -45,7 +45,7 @@
     3.4  
     3.5  Goal "!x. x : acc(r) ==> wf(r)";
     3.6  by (rtac wfUNIVI 1);
     3.7 -by(deepen_tac (claset() addEs [acc_induct]) 1 1);
     3.8 +by (deepen_tac (claset() addEs [acc_induct]) 1 1);
     3.9  qed "acc_wfI";
    3.10  
    3.11  Goal "wf(r) ==> x : acc(r)";
     4.1 --- a/src/HOL/Induct/Multiset0.ML	Wed Mar 03 11:12:29 1999 +0100
     4.2 +++ b/src/HOL/Induct/Multiset0.ML	Wed Mar 03 11:15:18 1999 +0100
     4.3 @@ -7,5 +7,5 @@
     4.4  *)
     4.5  
     4.6  Goal "(%x.0) : {f. finite {x. 0 < f x}}";
     4.7 -by(Simp_tac 1);
     4.8 +by (Simp_tac 1);
     4.9  qed "multiset_witness";
     5.1 --- a/src/HOL/Integ/Bin.ML	Wed Mar 03 11:12:29 1999 +0100
     5.2 +++ b/src/HOL/Integ/Bin.ML	Wed Mar 03 11:15:18 1999 +0100
     5.3 @@ -500,33 +500,33 @@
     5.4  
     5.5  (* Some test data
     5.6  Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
     5.7 -by(fast_arith_tac 1);
     5.8 +by (fast_arith_tac 1);
     5.9  Goal "!!a::int. [| a < b; c < d |] ==> a-d+ #2 <= b+(-c)";
    5.10 -by(fast_arith_tac 1);
    5.11 +by (fast_arith_tac 1);
    5.12  Goal "!!a::int. [| a < b; c < d |] ==> a+c+ #1 < b+d";
    5.13 -by(fast_arith_tac 1);
    5.14 +by (fast_arith_tac 1);
    5.15  Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c";
    5.16 -by(fast_arith_tac 1);
    5.17 +by (fast_arith_tac 1);
    5.18  Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \
    5.19  \     ==> a+a <= j+j";
    5.20 -by(fast_arith_tac 1);
    5.21 +by (fast_arith_tac 1);
    5.22  Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \
    5.23  \     ==> a+a - - #-1 < j+j - #3";
    5.24 -by(fast_arith_tac 1);
    5.25 +by (fast_arith_tac 1);
    5.26  Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
    5.27 -by(arith_tac 1);
    5.28 +by (arith_tac 1);
    5.29  Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
    5.30  \     ==> a <= l";
    5.31 -by(fast_arith_tac 1);
    5.32 +by (fast_arith_tac 1);
    5.33  Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
    5.34  \     ==> a+a+a+a <= l+l+l+l";
    5.35 -by(fast_arith_tac 1);
    5.36 +by (fast_arith_tac 1);
    5.37  Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
    5.38  \     ==> a+a+a+a+a <= l+l+l+l+i";
    5.39 -by(fast_arith_tac 1);
    5.40 +by (fast_arith_tac 1);
    5.41  Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
    5.42  \     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
    5.43 -by(fast_arith_tac 1);
    5.44 +by (fast_arith_tac 1);
    5.45  *)
    5.46  
    5.47  (*---------------------------------------------------------------------------*)
    5.48 @@ -548,50 +548,50 @@
    5.49  (** Simplification of inequalities involving numerical constants **)
    5.50  
    5.51  Goal "(w <= z + #1) = (w<=z | w = z + #1)";
    5.52 -by(arith_tac 1);
    5.53 +by (arith_tac 1);
    5.54  qed "zle_add1_eq";
    5.55  
    5.56  Goal "(w <= z - #1) = (w<z)";
    5.57 -by(arith_tac 1);
    5.58 +by (arith_tac 1);
    5.59  qed "zle_diff1_eq";
    5.60  Addsimps [zle_diff1_eq];
    5.61  
    5.62  (*2nd premise can be proved automatically if v is a literal*)
    5.63  Goal "[| w <= z; #0 <= v |] ==> w <= z + v";
    5.64 -by(fast_arith_tac 1);
    5.65 +by (fast_arith_tac 1);
    5.66  qed "zle_imp_zle_zadd";
    5.67  
    5.68  Goal "w <= z ==> w <= z + #1";
    5.69 -by(fast_arith_tac 1);
    5.70 +by (fast_arith_tac 1);
    5.71  qed "zle_imp_zle_zadd1";
    5.72  
    5.73  (*2nd premise can be proved automatically if v is a literal*)
    5.74  Goal "[| w < z; #0 <= v |] ==> w < z + v";
    5.75 -by(fast_arith_tac 1);
    5.76 +by (fast_arith_tac 1);
    5.77  qed "zless_imp_zless_zadd";
    5.78  
    5.79  Goal "w < z ==> w < z + #1";
    5.80 -by(fast_arith_tac 1);
    5.81 +by (fast_arith_tac 1);
    5.82  qed "zless_imp_zless_zadd1";
    5.83  
    5.84  Goal "(w < z + #1) = (w<=z)";
    5.85 -by(arith_tac 1);
    5.86 +by (arith_tac 1);
    5.87  qed "zle_add1_eq_le";
    5.88  Addsimps [zle_add1_eq_le];
    5.89  
    5.90  Goal "(z = z + w) = (w = #0)";
    5.91 -by(arith_tac 1);
    5.92 +by (arith_tac 1);
    5.93  qed "zadd_left_cancel0";
    5.94  Addsimps [zadd_left_cancel0];
    5.95  
    5.96  (*LOOPS as a simprule!*)
    5.97  Goal "[| w + v < z; #0 <= v |] ==> w < z";
    5.98 -by(fast_arith_tac 1);
    5.99 +by (fast_arith_tac 1);
   5.100  qed "zless_zadd_imp_zless";
   5.101  
   5.102  (*LOOPS as a simprule!  Analogous to Suc_lessD*)
   5.103  Goal "w + #1 < z ==> w < z";
   5.104 -by(fast_arith_tac 1);
   5.105 +by (fast_arith_tac 1);
   5.106  qed "zless_zadd1_imp_zless";
   5.107  
   5.108  Goal "w + #-1 = w - #1";
     6.1 --- a/src/HOL/Lambda/Eta.ML	Wed Mar 03 11:12:29 1999 +0100
     6.2 +++ b/src/HOL/Lambda/Eta.ML	Wed Mar 03 11:15:18 1999 +0100
     6.3 @@ -28,8 +28,8 @@
     6.4  Goal "!i k. free (lift t k) i = (i < k & free t i | k < i & free t (i-1))";
     6.5  by (induct_tac "t" 1);
     6.6    by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()) addcongs [conj_cong])));
     6.7 - by(arith_tac 1);
     6.8 -by(Auto_tac);
     6.9 + by (arith_tac 1);
    6.10 +by (Auto_tac);
    6.11  qed "free_lift";
    6.12  Addsimps [free_lift];
    6.13  
    6.14 @@ -115,7 +115,7 @@
    6.15  
    6.16  Goal "!i. t[Var i/i] = t[Var(i)/Suc i]";
    6.17  by (induct_tac "t" 1);
    6.18 -by(auto_tac (claset() addSEs [linorder_neqE], addsplit (simpset())));
    6.19 +by (auto_tac (claset() addSEs [linorder_neqE], addsplit (simpset())));
    6.20  qed_spec_mp "subst_Var_Suc";
    6.21  Addsimps [subst_Var_Suc];
    6.22  
     7.1 --- a/src/HOL/Lambda/ListApplication.ML	Wed Mar 03 11:12:29 1999 +0100
     7.2 +++ b/src/HOL/Lambda/ListApplication.ML	Wed Mar 03 11:15:18 1999 +0100
     7.3 @@ -88,7 +88,7 @@
     7.4  Addsimps [size_apps];
     7.5  
     7.6  Goal "[| 0 < k; m <= n |] ==> m < n+k";
     7.7 -by(fast_arith_tac 1);
     7.8 +by (fast_arith_tac 1);
     7.9  val lemma = result();
    7.10  
    7.11  (* a customized induction schema for $$ *)
     8.1 --- a/src/HOL/Lex/NA.ML	Wed Mar 03 11:12:29 1999 +0100
     8.2 +++ b/src/HOL/Lex/NA.ML	Wed Mar 03 11:15:18 1999 +0100
     8.3 @@ -7,23 +7,23 @@
     8.4  Goal
     8.5   "steps A (v@w) = steps A w  O  steps A v";
     8.6  by (induct_tac "v" 1);
     8.7 -by(ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
     8.8 +by (ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
     8.9  qed "steps_append";
    8.10  Addsimps [steps_append];
    8.11  
    8.12  Goal "(p,r) : steps A (v@w) = ((p,r) : (steps A w O steps A v))";
    8.13 -by(rtac (steps_append RS equalityE) 1);
    8.14 -by(Blast_tac 1);
    8.15 +by (rtac (steps_append RS equalityE) 1);
    8.16 +by (Blast_tac 1);
    8.17  qed "in_steps_append";
    8.18  AddIffs [in_steps_append];
    8.19  
    8.20  Goal
    8.21   "!p. delta A w p = {q. (p,q) : steps A w}";
    8.22 -by(induct_tac "w" 1);
    8.23 -by(auto_tac (claset(), simpset() addsimps [step_def]));
    8.24 +by (induct_tac "w" 1);
    8.25 +by (auto_tac (claset(), simpset() addsimps [step_def]));
    8.26  qed_spec_mp "delta_conv_steps";
    8.27  
    8.28  Goalw [accepts_def]
    8.29   "accepts A w = (? q. (start A,q) : steps A w & fin A q)";
    8.30 -by(simp_tac (simpset() addsimps [delta_conv_steps]) 1);
    8.31 +by (simp_tac (simpset() addsimps [delta_conv_steps]) 1);
    8.32  qed "accepts_conv_steps";
     9.1 --- a/src/HOL/Map.ML	Wed Mar 03 11:12:29 1999 +0100
     9.2 +++ b/src/HOL/Map.ML	Wed Mar 03 11:15:18 1999 +0100
     9.3 @@ -120,7 +120,7 @@
     9.4  	Asm_full_simp_tac 1]);
     9.5  
     9.6  Goalw [dom_def] "dom(m++n) = dom n Un dom m";
     9.7 -by(Simp_tac 1);
     9.8 +by (Simp_tac 1);
     9.9  by (Blast_tac 1);
    9.10  qed "dom_override";
    9.11  Addsimps [dom_override];
    10.1 --- a/src/HOL/Nat.ML	Wed Mar 03 11:12:29 1999 +0100
    10.2 +++ b/src/HOL/Nat.ML	Wed Mar 03 11:15:18 1999 +0100
    10.3 @@ -39,8 +39,8 @@
    10.4  AddIffs [neq0_conv];
    10.5  
    10.6  Goal "(0 ~= n) = (0 < n)";
    10.7 -by(exhaust_tac "n" 1);
    10.8 -by(Auto_tac);
    10.9 +by (exhaust_tac "n" 1);
   10.10 +by (Auto_tac);
   10.11  qed "zero_neq_conv";
   10.12  AddIffs [zero_neq_conv];
   10.13  
    11.1 --- a/src/HOL/Ord.ML	Wed Mar 03 11:12:29 1999 +0100
    11.2 +++ b/src/HOL/Ord.ML	Wed Mar 03 11:15:18 1999 +0100
    11.3 @@ -161,10 +161,10 @@
    11.4  
    11.5  Goalw [min_def]
    11.6   "P(min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))";
    11.7 -by(Simp_tac 1);
    11.8 +by (Simp_tac 1);
    11.9  qed "split_min";
   11.10  
   11.11  Goalw [max_def]
   11.12   "P(max (i::'a::linorder) j) = ((i <= j --> P(j)) & (~ i <= j --> P(i)))";
   11.13 -by(Simp_tac 1);
   11.14 +by (Simp_tac 1);
   11.15  qed "split_max";
    12.1 --- a/src/HOL/Set.ML	Wed Mar 03 11:12:29 1999 +0100
    12.2 +++ b/src/HOL/Set.ML	Wed Mar 03 11:15:18 1999 +0100
    12.3 @@ -467,7 +467,7 @@
    12.4  Addsimps [singleton_conv];
    12.5  
    12.6  Goal "{x. a=x} = {a}";
    12.7 -by(Blast_tac 1);
    12.8 +by (Blast_tac 1);
    12.9  qed "singleton_conv2";
   12.10  Addsimps [singleton_conv2];
   12.11  
    13.1 --- a/src/HOL/TLA/Action.ML	Wed Mar 03 11:12:29 1999 +0100
    13.2 +++ b/src/HOL/TLA/Action.ML	Wed Mar 03 11:15:18 1999 +0100
    13.3 @@ -253,6 +253,6 @@
    13.4  
    13.5  val [prem] = goal thy "basevars (x,y,z) ==> |- x --> Enabled ($x & (y$ = #False))";
    13.6  by (enabled_tac prem 1);
    13.7 -auto();
    13.8 +by Auto_tac;
    13.9  
   13.10  *)
    14.1 --- a/src/HOL/equalities.ML	Wed Mar 03 11:12:29 1999 +0100
    14.2 +++ b/src/HOL/equalities.ML	Wed Mar 03 11:15:18 1999 +0100
    14.3 @@ -747,7 +747,7 @@
    14.4  qed "ex_bool_eq";
    14.5  
    14.6  Goal "A Un B = (UN b. if b then A else B)";
    14.7 -by(auto_tac(claset()delWrapper"bspec",simpset()addsimps [split_if_mem2]));
    14.8 +by (auto_tac(claset()delWrapper"bspec",simpset()addsimps [split_if_mem2]));
    14.9  qed "Un_eq_UN";
   14.10  
   14.11  Goal "(UN b::bool. A b) = (A True Un A False)";
    15.1 --- a/src/HOL/simpdata.ML	Wed Mar 03 11:12:29 1999 +0100
    15.2 +++ b/src/HOL/simpdata.ML	Wed Mar 03 11:15:18 1999 +0100
    15.3 @@ -498,7 +498,7 @@
    15.4        val refute_prems_tac =
    15.5          REPEAT(eresolve_tac [conjE, exE] 1 ORELSE
    15.6                 filter_prems_tac test 1 ORELSE
    15.7 -               eresolve_tac [disjE] 1) THEN
    15.8 +               etac disjE 1) THEN
    15.9          ref_tac 1;
   15.10    in EVERY'[TRY o filter_prems_tac test,
   15.11              DETERM o REPEAT o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac,