# 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.*)