# HG changeset patch
# User wenzelm
# Date 939041135 -7200
# Node ID 27676b51243d65760f54ff1e396fefdb4ee09e66
# Parent  affe0c2fdfbff141c309e512778b8ef995fc5153
added mk_conj, mk_disj, mk_imp;

diff -r affe0c2fdfbf -r 27676b51243d src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Mon Oct 04 13:47:28 1999 +0200
+++ b/src/HOL/hologic.ML	Mon Oct 04 14:45:35 1999 +0200
@@ -20,6 +20,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 eq_const: typ -> term
   val all_const: typ -> term
@@ -102,6 +105,10 @@
 and disj = Const ("op |", [boolT, boolT] ---> boolT)
 and imp = Const ("op -->", [boolT, boolT] ---> boolT);
 
+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]);