added subsig: sg * sg -> bool to test if one signature is contained in another.
authornipkow
Thu Dec 30 10:18:23 1993 +0100 (1993-12-30)
changeset 2060d624d1ba9cc
parent 205 0dd3a0a264cd
child 207 059e406442fd
added subsig: sg * sg -> bool to test if one signature is contained in another.
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Wed Dec 29 10:14:58 1993 +0100
     1.2 +++ b/src/Pure/sign.ML	Thu Dec 30 10:18:23 1993 +0100
     1.3 @@ -46,6 +46,7 @@
     1.4    val pprint_ctyp: ctyp -> pprint_args -> unit
     1.5    val string_of_term: sg -> term -> string
     1.6    val string_of_typ: sg -> typ -> string
     1.7 +  val subsig: sg * sg -> bool
     1.8    val pprint_term: sg -> term -> pprint_args -> unit
     1.9    val pprint_typ: sg -> typ -> pprint_args -> unit
    1.10    val term_of: cterm -> term
    1.11 @@ -74,6 +75,8 @@
    1.12  
    1.13  fun rep_sg (Sg args) = args;
    1.14  
    1.15 +fun subsig(Sg{stamps=s1,...},Sg{stamps=s2,...}) = s1 subset s2;
    1.16 +
    1.17  fun string_of_typ(Sg{tsig,syn,...}) = Syntax.string_of_typ syn;
    1.18  
    1.19  fun pprint_typ(Sg{syn,...}) = Pretty.pprint o Pretty.quote o (Syntax.pretty_typ syn);