src/Pure/sorts.ML

 minimal classes (wrt. current class inclusion).
 *)
 
 signature SORTS =
 sig
+  val subset: sort OrdList.T * sort OrdList.T -> bool
   val union: sort OrdList.T -> sort OrdList.T -> sort OrdList.T
   val subtract: sort OrdList.T -> sort OrdList.T -> sort OrdList.T
   val remove_sort: sort -> sort OrdList.T -> sort OrdList.T
   val insert_sort: sort -> sort OrdList.T -> sort OrdList.T
   val insert_typ: typ -> sort OrdList.T -> sort OrdList.T

 struct
 
 
 (** ordered lists of sorts **)
 
+val op subset = OrdList.subset Term.sort_ord;
 val op union = OrdList.union Term.sort_ord;
 val subtract = OrdList.subtract Term.sort_ord;
 
 val remove_sort = OrdList.remove Term.sort_ord;
 val insert_sort = OrdList.insert Term.sort_ord;