# HG changeset patch
# User wenzelm
# Date 1005510651 -3600
# Node ID 6123958975b8d1a97bf656433152bbd80daf2829
# Parent  74156e7bb22ef4325eebccec2387812fdd715c62
added mk_conjunction;

diff -r 74156e7bb22e -r 6123958975b8 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Sun Nov 11 21:30:31 2001 +0100
+++ b/src/Pure/logic.ML	Sun Nov 11 21:30:51 2001 +0100
@@ -22,6 +22,7 @@
   val strip_imp_concl   : term -> term
   val strip_prems       : int * term list * term -> term list * term
   val count_prems       : term * int -> int
+  val mk_conjunction    : term * term -> term
   val mk_flexpair       : term * term -> term
   val dest_flexpair     : term -> term * term
   val list_flexpairs    : (term*term)list * term -> term
@@ -118,6 +119,13 @@
   | count_prems (_,n) = n;
 
 
+(** conjunction **)
+
+fun mk_conjunction (t, u) =
+  Term.list_all ([("C", propT)], mk_implies (list_implies ([t, u], Bound 0), Bound 0));
+
+
+
 (** flex-flex constraints **)
 
 (*Make a constraint.*)