added is_equals: term -> bool;
authorwenzelm
Wed Oct 12 16:31:01 1994 +0100 (1994-10-12)
changeset 637b344bf624143
parent 636 31b36d96f7d6
child 638 7f25cc9067e7
added is_equals: term -> bool;
src/Pure/logic.ML
     1.1 --- a/src/Pure/logic.ML	Wed Oct 12 16:30:19 1994 +0100
     1.2 +++ b/src/Pure/logic.ML	Wed Oct 12 16:31:01 1994 +0100
     1.3 @@ -26,6 +26,7 @@
     1.4    val list_flexpairs	: (term*term)list * term -> term
     1.5    val list_implies	: term list * term -> term
     1.6    val list_rename_params: string list * term -> term
     1.7 +  val is_equals         : term -> bool
     1.8    val mk_equals		: term * term -> term
     1.9    val mk_flexpair	: term * term -> term
    1.10    val mk_implies	: term * term -> term
    1.11 @@ -64,6 +65,10 @@
    1.12  fun dest_equals (Const("==",_) $ t $ u)  =  (t,u)
    1.13    | dest_equals t = raise TERM("dest_equals", [t]);
    1.14  
    1.15 +fun is_equals (Const ("==", _) $ _ $ _) = true
    1.16 +  | is_equals _ = false;
    1.17 +
    1.18 +
    1.19  (** implies **)
    1.20  
    1.21  fun mk_implies(A,B) = implies $ A $ B;