# 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]);