splitter setup;
authorwenzelm
Wed Mar 15 18:47:28 2000 +0100 (2000-03-15)
changeset 84732798d2f71ec2
parent 8472 50a653f8b8ea
child 8474 ae32be343647
splitter setup;
src/HOL/HOL.thy
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/HOL.thy	Wed Mar 15 18:42:54 2000 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Mar 15 18:47:28 2000 +0100
     1.3 @@ -188,7 +188,9 @@
     1.4  use "HOL_lemmas.ML"	setup attrib_setup
     1.5  use "cladata.ML"	setup Classical.setup setup clasetup
     1.6  use "blastdata.ML"	setup Blast.setup
     1.7 -use "simpdata.ML"	setup Simplifier.setup setup iff_attrib_setup
     1.8 +use "simpdata.ML"	setup Simplifier.setup
     1.9 +			setup "Simplifier.method_setup Splitter.split_modifiers"
    1.10 +                        setup Splitter.setup setup iff_attrib_setup
    1.11  			setup simpsetup setup Clasimp.setup
    1.12  
    1.13  
     2.1 --- a/src/HOL/simpdata.ML	Wed Mar 15 18:42:54 2000 +0100
     2.2 +++ b/src/HOL/simpdata.ML	Wed Mar 15 18:47:28 2000 +0100
     2.3 @@ -517,9 +517,8 @@
     2.4  (*** integration of simplifier with classical reasoner ***)
     2.5  
     2.6  structure Clasimp = ClasimpFun
     2.7 - (structure Simplifier = Simplifier 
     2.8 -        and Classical  = Classical 
     2.9 -        and Blast      = Blast);
    2.10 + (structure Simplifier = Simplifier and Splitter = Splitter
    2.11 +   and Classical  = Classical and Blast = Blast);
    2.12  open Clasimp;
    2.13  
    2.14  val HOL_css = (HOL_cs, HOL_ss);