diff -r 78abd4c4802a -r a1d0a6d555cd src/Pure/logic.ML
--- a/src/Pure/logic.ML	Tue Jun 16 18:37:34 1998 +0200
+++ b/src/Pure/logic.ML	Wed Jun 17 10:48:38 1998 +0200
@@ -21,7 +21,9 @@
   val dest_type		: term -> typ
   val flatten_params	: int -> term -> term
   val incr_indexes	: typ list * int -> term -> term
+  val is_all            : term -> bool
   val is_equals         : term -> bool
+  val is_implies        : term -> bool
   val lift_fns		: term * int -> (term -> term) * (term -> term)
   val list_flexpairs	: (term*term)list * term -> term
   val list_implies	: term list * term -> term
@@ -55,6 +57,12 @@
 
 (*** Abstract syntax operations on the meta-connectives ***)
 
+(** all **)
+
+fun is_all (Const ("all", _) $ _) = true
+  | is_all _ = false;
+
+
 (** equality **)
 
 (*Make an equality.  DOES NOT CHECK TYPE OF u*)
@@ -74,6 +82,9 @@
 fun dest_implies (Const("==>",_) $ A $ B)  =  (A,B)
   | dest_implies A = raise TERM("dest_implies", [A]);
 
+fun is_implies (Const ("==>", _) $ _ $ _) = true
+  | is_implies _ = false;
+
 
 (** nested implications **)