# HG changeset patch
# User wenzelm
# Date 781975861 -3600
# Node ID b344bf6241432f6453dd6cf2f28314ad8ed16711
# Parent  31b36d96f7d6c50209334912ec50e395497f6625
added is_equals: term -> bool;

diff -r 31b36d96f7d6 -r b344bf624143 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Wed Oct 12 16:30:19 1994 +0100
+++ b/src/Pure/logic.ML	Wed Oct 12 16:31:01 1994 +0100
@@ -26,6 +26,7 @@
   val list_flexpairs	: (term*term)list * term -> term
   val list_implies	: term list * term -> term
   val list_rename_params: string list * term -> term
+  val is_equals         : term -> bool
   val mk_equals		: term * term -> term
   val mk_flexpair	: term * term -> term
   val mk_implies	: term * term -> term
@@ -64,6 +65,10 @@
 fun dest_equals (Const("==",_) $ t $ u)  =  (t,u)
   | dest_equals t = raise TERM("dest_equals", [t]);
 
+fun is_equals (Const ("==", _) $ _ $ _) = true
+  | is_equals _ = false;
+
+
 (** implies **)
 
 fun mk_implies(A,B) = implies $ A $ B;