# HG changeset patch
# User wenzelm
# Date 968352722 -7200
# Node ID 75e55370b1aef5ffa6b82c234609520cd7f598d9
# Parent  c8ff37b637a7b93a4289e63806f3f31d8a04b187
added linorder_cases;
added Rulify.setup;

diff -r c8ff37b637a7 -r 75e55370b1ae src/HOL/subset.thy
--- 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