added linorder_cases;
added Rulify.setup;

--- a/src/HOL/subset.thy	Thu Sep 07 20:51:31 2000 +0200
+++ b/src/HOL/subset.thy	Thu Sep 07 20:52:02 2000 +0200
@@ -7,6 +7,11 @@
 theory subset = Set
 files "Tools/typedef_package.ML":
 
-setup rulify_prems_attrib_setup
+(*belongs to theory Ord*)
+theorems linorder_cases [case_names less equal greater] =
+  linorder_less_split
+
+(*belongs to theory Set*)
+setup Rulify.setup
 
 end