# HG changeset patch
# User wenzelm
# Date 953142448 -3600
# Node ID 2798d2f71ec2cfd6e9fbb30ceb7799f28787c037
# Parent  50a653f8b8ea0ddd27b9eba7f1a353b724f3b8a2
splitter setup;

diff -r 50a653f8b8ea -r 2798d2f71ec2 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Mar 15 18:42:54 2000 +0100
+++ b/src/HOL/HOL.thy	Wed Mar 15 18:47:28 2000 +0100
@@ -188,7 +188,9 @@
 use "HOL_lemmas.ML"	setup attrib_setup
 use "cladata.ML"	setup Classical.setup setup clasetup
 use "blastdata.ML"	setup Blast.setup
-use "simpdata.ML"	setup Simplifier.setup setup iff_attrib_setup
+use "simpdata.ML"	setup Simplifier.setup
+			setup "Simplifier.method_setup Splitter.split_modifiers"
+                        setup Splitter.setup setup iff_attrib_setup
 			setup simpsetup setup Clasimp.setup
 
 
diff -r 50a653f8b8ea -r 2798d2f71ec2 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Wed Mar 15 18:42:54 2000 +0100
+++ b/src/HOL/simpdata.ML	Wed Mar 15 18:47:28 2000 +0100
@@ -517,9 +517,8 @@
 (*** integration of simplifier with classical reasoner ***)
 
 structure Clasimp = ClasimpFun
- (structure Simplifier = Simplifier 
-        and Classical  = Classical 
-        and Blast      = Blast);
+ (structure Simplifier = Simplifier and Splitter = Splitter
+   and Classical  = Classical and Blast = Blast);
 open Clasimp;
 
 val HOL_css = (HOL_cs, HOL_ss);