src/Pure/drule.ML
changeset 9547 8dad21f06b24
parent 9460 53d7ad5bec39
child 9554 1b0f02abbde8
     1.1 --- a/src/Pure/drule.ML	Mon Aug 07 10:28:32 2000 +0200
     1.2 +++ b/src/Pure/drule.ML	Mon Aug 07 10:29:04 2000 +0200
     1.3 @@ -10,6 +10,8 @@
     1.4  
     1.5  signature BASIC_DRULE =
     1.6  sig
     1.7 +  val mk_implies        : cterm * cterm -> cterm
     1.8 +  val list_implies      : cterm list * cterm -> cterm
     1.9    val dest_implies      : cterm -> cterm * cterm
    1.10    val skip_flexpairs    : cterm -> cterm
    1.11    val strip_imp_prems   : cterm -> cterm list
    1.12 @@ -151,6 +153,17 @@
    1.13  (*The premises of a theorem, as a cterm list*)
    1.14  val cprems_of = strip_imp_prems o skip_flexpairs o cprop_of;
    1.15  
    1.16 +val proto_sign = Theory.sign_of ProtoPure.thy;
    1.17 +
    1.18 +val implies = cterm_of proto_sign Term.implies;
    1.19 +
    1.20 +(*cterm version of mk_implies*)
    1.21 +fun mk_implies(A,B) = capply (capply implies A) B;
    1.22 +
    1.23 +(*cterm version of list_implies: [A1,...,An], B  goes to [|A1;==>;An|]==>B *)
    1.24 +fun list_implies([], B) = B
    1.25 +  | list_implies(A::AS, B) = mk_implies (A, list_implies(AS,B));
    1.26 +
    1.27  
    1.28  (** reading of instantiations **)
    1.29  
    1.30 @@ -435,8 +448,6 @@
    1.31  
    1.32  (*** Meta-Rewriting Rules ***)
    1.33  
    1.34 -val proto_sign = Theory.sign_of ProtoPure.thy;
    1.35 -
    1.36  fun read_prop s = read_cterm proto_sign (s, propT);
    1.37  
    1.38  fun store_thm name thm = hd (PureThy.smart_store_thms (name, [thm]));
    1.39 @@ -460,7 +471,7 @@
    1.40  
    1.41  (** Below, a "conversion" has type cterm -> thm **)
    1.42  
    1.43 -val refl_implies = reflexive (cterm_of proto_sign implies);
    1.44 +val refl_implies = reflexive implies;
    1.45  
    1.46  (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
    1.47  (*Do not rewrite flex-flex pairs*)