replaced fn _ => by K
authoroheimb
Thu Jan 08 17:42:26 1998 +0100 (1998-01-08)
changeset 4525b96b513c6c65
parent 4524 7399288f5dd3
child 4526 6be35399125a
replaced fn _ => by K
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Thu Jan 08 16:52:31 1998 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Thu Jan 08 17:42:26 1998 +0100
     1.3 @@ -54,7 +54,7 @@
     1.4  
     1.5  local
     1.6  
     1.7 -  fun prover s = prove_goal HOL.thy s (fn _ => [blast_tac HOL_cs 1]);
     1.8 +  fun prover s = prove_goal HOL.thy s (K [blast_tac HOL_cs 1]);
     1.9  
    1.10    val P_imp_P_iff_True = prover "P --> (P = True)" RS mp;
    1.11    val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
    1.12 @@ -166,11 +166,11 @@
    1.13  
    1.14  val True_implies_equals = prove_goal HOL.thy
    1.15   "(True ==> PROP P) == PROP P"
    1.16 -(fn _ => [rtac equal_intr_rule 1, atac 2,
    1.17 +(K [rtac equal_intr_rule 1, atac 2,
    1.18            METAHYPS (fn prems => resolve_tac prems 1) 1,
    1.19            rtac TrueI 1]);
    1.20  
    1.21 -fun prove nm thm  = qed_goal nm HOL.thy thm (fn _ => [blast_tac HOL_cs 1]);
    1.22 +fun prove nm thm  = qed_goal nm HOL.thy thm (K [blast_tac HOL_cs 1]);
    1.23  
    1.24  prove "conj_commute" "(P&Q) = (Q&P)";
    1.25  prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))";
    1.26 @@ -239,16 +239,16 @@
    1.27  prove "eq_sym_conv" "(x=y) = (y=x)";
    1.28  
    1.29  qed_goalw "o_apply" HOL.thy [o_def] "(f o g) x = f (g x)"
    1.30 - (fn _ => [rtac refl 1]);
    1.31 + (K [rtac refl 1]);
    1.32  
    1.33  qed_goal "meta_eq_to_obj_eq" HOL.thy "x==y ==> x=y"
    1.34    (fn [prem] => [rewtac prem, rtac refl 1]);
    1.35  
    1.36  qed_goalw "if_True" HOL.thy [if_def] "(if True then x else y) = x"
    1.37 - (fn _=>[blast_tac (HOL_cs addIs [select_equality]) 1]);
    1.38 + (K [Blast_tac 1]);
    1.39  
    1.40  qed_goalw "if_False" HOL.thy [if_def] "(if False then x else y) = y"
    1.41 - (fn _=>[blast_tac (HOL_cs addIs [select_equality]) 1]);
    1.42 + (K [Blast_tac 1]);
    1.43  
    1.44  qed_goal "if_P" HOL.thy "P ==> (if P then x else y) = x"
    1.45   (fn [prem] => [ stac (prem RS eqTrueI) 1, rtac if_True 1 ]);
    1.46 @@ -257,7 +257,7 @@
    1.47   (fn [prem] => [ stac (prem RS not_P_imp_P_iff_F) 1, rtac if_False 1 ]);
    1.48  *)
    1.49  qed_goalw "if_not_P" HOL.thy [if_def] "!!P. ~P ==> (if P then x else y) = y"
    1.50 - (fn _ => [blast_tac (HOL_cs addIs [select_equality]) 1]);
    1.51 + (K [Blast_tac 1]);
    1.52  
    1.53  qed_goal "expand_if" HOL.thy
    1.54      "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))" (K [
    1.55 @@ -273,7 +273,7 @@
    1.56  
    1.57  qed_goal "if_bool_eq" HOL.thy
    1.58                     "(if P then Q else R) = ((P-->Q) & (~P-->R))"
    1.59 -                   (fn _ => [rtac expand_if 1]);
    1.60 +                   (K [rtac expand_if 1]);
    1.61  
    1.62  
    1.63  (*** make simplification procedures for quantifier elimination ***)
    1.64 @@ -337,7 +337,7 @@
    1.65  
    1.66  
    1.67  qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
    1.68 -  (fn _ => [split_tac [expand_if] 1, blast_tac HOL_cs 1]);
    1.69 +  (K [split_tac [expand_if] 1, blast_tac HOL_cs 1]);
    1.70  
    1.71  (** 'if' congruence rules: neither included by default! *)
    1.72  
    1.73 @@ -395,10 +395,10 @@
    1.74  
    1.75  qed_goal "if_distrib" HOL.thy
    1.76    "f(if c then x else y) = (if c then f x else f y)" 
    1.77 -  (fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);
    1.78 +  (K [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);
    1.79  
    1.80  qed_goalw "o_assoc" HOL.thy [o_def] "f o (g o h) = f o g o h"
    1.81 -  (fn _ => [rtac ext 1, rtac refl 1]);
    1.82 +  (K [rtac ext 1, rtac refl 1]);
    1.83  
    1.84  
    1.85  (*For expand_case_tac*)