# HG changeset patch
# User wenzelm
# Date 939065726 -7200
# Node ID 89bbce6f5c17b275d3ad0e86fa21d5956b8a0098
# Parent  b7e8277fa088110b0699860ba3fa5b0384e7129a
added mk_conj, mk_disj, mk_imp;

diff -r b7e8277fa088 -r 89bbce6f5c17 src/FOL/fologic.ML
--- a/src/FOL/fologic.ML	Mon Oct 04 21:34:20 1999 +0200
+++ b/src/FOL/fologic.ML	Mon Oct 04 21:35:26 1999 +0200
@@ -13,6 +13,9 @@
   val conj		: term
   val disj		: term
   val imp		: term
+  val mk_conj		: term * term -> term
+  val mk_disj		: term * term -> term
+  val mk_imp		: term * term -> term
   val dest_imp	       	: term -> term*term
   val all_const		: typ -> term
   val mk_all		: term * term -> term
@@ -42,6 +45,10 @@
 and disj = Const("op |", [oT,oT]--->oT)
 and imp = Const("op -->", [oT,oT]--->oT);
 
+fun mk_conj (t1, t2) = conj $ t1 $ t2
+and mk_disj (t1, t2) = disj $ t1 $ t2
+and mk_imp (t1, t2) = imp $ t1 $ t2;
+
 fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
   | dest_imp  t = raise TERM ("dest_imp", [t]);