# 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);