# HG changeset patch
# User wenzelm
# Date 1222442655 -7200
# Node ID 27f1b5cc5f9bcd162d477d9e4a5f80ac43906847
# Parent  5e2c526cfaf03a744437aa5ff0945edb0102d196
added subset operation;

diff -r 5e2c526cfaf0 -r 27f1b5cc5f9b src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Fri Sep 26 14:53:10 2008 +0200
+++ b/src/Pure/sorts.ML	Fri Sep 26 17:24:15 2008 +0200
@@ -15,6 +15,7 @@
 
 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
@@ -67,6 +68,7 @@
 
 (** 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;