--- a/src/FOL/fologic.ML Tue Jan 19 11:16:07 1999 +0100
+++ b/src/FOL/fologic.ML Tue Jan 19 11:16:39 1999 +0100
@@ -7,19 +7,20 @@
signature FOLOGIC =
sig
- 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
- val eq_const: typ -> term
- val all_const: typ -> term
- val exists_const: typ -> term
- val mk_eq: term * term -> term
- val mk_all: term * term -> term
- val mk_exists: term * term -> term
+ val oT : typ
+ val mk_Trueprop : term -> term
+ val dest_Trueprop : term -> term
+ val conj : term
+ val disj : term
+ val imp : term
+ val dest_imp : term -> term*term
+ val all_const : typ -> term
+ val mk_all : term * term -> term
+ val exists_const : typ -> term
+ val mk_exists : term * term -> term
+ val eq_const : typ -> term
+ val mk_eq : term * term -> term
+ val dest_eq : term -> term*term
end;
@@ -47,6 +48,9 @@
fun eq_const T = Const ("op =", [T, T] ---> oT);
fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
+fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs)
+ | dest_eq t = raise TERM ("dest_eq", [t])
+
fun all_const T = Const ("All", [T --> oT] ---> oT);
fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P));