# HG changeset patch
# User nipkow
# Date 757243103 -3600
# Node ID 0d624d1ba9ccce22fd9625d655c5c8bb79e4e76b
# Parent  0dd3a0a264cdd43e7ce36823d41063dbef544712
added subsig: sg * sg -> bool to test if one signature is contained in another.

diff -r 0dd3a0a264cd -r 0d624d1ba9cc src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Dec 29 10:14:58 1993 +0100
+++ b/src/Pure/sign.ML	Thu Dec 30 10:18:23 1993 +0100
@@ -46,6 +46,7 @@
   val pprint_ctyp: ctyp -> pprint_args -> unit
   val string_of_term: sg -> term -> string
   val string_of_typ: sg -> typ -> string
+  val subsig: sg * sg -> bool
   val pprint_term: sg -> term -> pprint_args -> unit
   val pprint_typ: sg -> typ -> pprint_args -> unit
   val term_of: cterm -> term
@@ -74,6 +75,8 @@
 
 fun rep_sg (Sg args) = args;
 
+fun subsig(Sg{stamps=s1,...},Sg{stamps=s2,...}) = s1 subset s2;
+
 fun string_of_typ(Sg{tsig,syn,...}) = Syntax.string_of_typ syn;
 
 fun pprint_typ(Sg{syn,...}) = Pretty.pprint o Pretty.quote o (Syntax.pretty_typ syn);