--- a/src/FOL/fologic.ML Tue Dec 23 11:37:48 1997 +0100
+++ b/src/FOL/fologic.ML Tue Dec 23 11:39:03 1997 +0100
@@ -10,6 +10,7 @@
val oT: typ
val mk_Trueprop: term -> term
val dest_Trueprop: term -> term
+ val dest_imp : term -> term*term
val conj: term
val disj: term
val imp: term
@@ -40,6 +41,9 @@
and disj = Const("op |", [oT,oT]--->oT)
and imp = Const("op -->", [oT,oT]--->oT);
+fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
+ | dest_imp t = raise TERM ("dest_imp", [t]);
+
fun eq_const T = Const ("op =", [T, T] ---> oT);
fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;