Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added mk_conjunction_list;
authorwenzelm
Tue, 15 Jan 2002 00:09:54 +0100
changeset 12757 b76a4376cfcb
parent 12756 08bf3d911968
child 12758 f6aceb9d4b8e
added mk_conjunction_list;
src/Pure/logic.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/logic.ML	Tue Jan 15 00:09:29 2002 +0100
+++ b/src/Pure/logic.ML	Tue Jan 15 00:09:54 2002 +0100
@@ -23,6 +23,7 @@
   val strip_prems       : int * term list * term -> term list * term
   val count_prems       : term * int -> int
   val mk_conjunction    : term * term -> term
+  val mk_conjunction_list: term list -> term
   val mk_flexpair       : term * term -> term
   val dest_flexpair     : term -> term * term
   val list_flexpairs    : (term*term)list * term -> term
@@ -124,6 +125,8 @@
 fun mk_conjunction (t, u) =
   Term.list_all ([("C", propT)], mk_implies (list_implies ([t, u], Bound 0), Bound 0));
 
+fun mk_conjunction_list [] = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0))
+  | mk_conjunction_list ts = foldr1 mk_conjunction ts;
 
 
 (** flex-flex constraints **)
isabelle