--- a/src/HOL/hologic.ML Tue Dec 23 11:37:48 1997 +0100
+++ b/src/HOL/hologic.ML Tue Dec 23 11:39:03 1997 +0100
@@ -18,6 +18,7 @@
val conj: term
val disj: term
val imp: term
+ val dest_imp : term -> term*term
val eq_const: typ -> term
val all_const: typ -> term
val exists_const: typ -> term
@@ -73,6 +74,9 @@
and disj = Const ("op |", [boolT, boolT] ---> boolT)
and imp = Const ("op -->", [boolT, boolT] ---> boolT);
+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] ---> boolT);
fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;