# HG changeset patch
# User paulson
# Date 965636944 -7200
# Node ID 8dad21f06b24a4dcfe7e601378c9ddcbfa4d754c
# Parent  be095014e72f26ab39f0ebd75bd96bf67f1e6523
more cterm operations: mk_implies, list_implies

diff -r be095014e72f -r 8dad21f06b24 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Mon Aug 07 10:28:32 2000 +0200
+++ b/src/Pure/drule.ML	Mon Aug 07 10:29:04 2000 +0200
@@ -10,6 +10,8 @@
 
 signature BASIC_DRULE =
 sig
+  val mk_implies        : cterm * cterm -> cterm
+  val list_implies      : cterm list * cterm -> cterm
   val dest_implies      : cterm -> cterm * cterm
   val skip_flexpairs    : cterm -> cterm
   val strip_imp_prems   : cterm -> cterm list
@@ -151,6 +153,17 @@
 (*The premises of a theorem, as a cterm list*)
 val cprems_of = strip_imp_prems o skip_flexpairs o cprop_of;
 
+val proto_sign = Theory.sign_of ProtoPure.thy;
+
+val implies = cterm_of proto_sign Term.implies;
+
+(*cterm version of mk_implies*)
+fun mk_implies(A,B) = capply (capply implies A) B;
+
+(*cterm version of list_implies: [A1,...,An], B  goes to [|A1;==>;An|]==>B *)
+fun list_implies([], B) = B
+  | list_implies(A::AS, B) = mk_implies (A, list_implies(AS,B));
+
 
 (** reading of instantiations **)
 
@@ -435,8 +448,6 @@
 
 (*** Meta-Rewriting Rules ***)
 
-val proto_sign = Theory.sign_of ProtoPure.thy;
-
 fun read_prop s = read_cterm proto_sign (s, propT);
 
 fun store_thm name thm = hd (PureThy.smart_store_thms (name, [thm]));
@@ -460,7 +471,7 @@
 
 (** Below, a "conversion" has type cterm -> thm **)
 
-val refl_implies = reflexive (cterm_of proto_sign implies);
+val refl_implies = reflexive implies;
 
 (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
 (*Do not rewrite flex-flex pairs*)