src/HOL/Transitive_Closure.thy
changeset 42795 66fcc9882784
parent 41987 4ad8f1dc2e0b
child 43596 78211f66cf8d
     1.1 --- a/src/HOL/Transitive_Closure.thy	Fri May 13 23:24:06 2011 +0200
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Fri May 13 23:58:40 2011 +0200
     1.3 @@ -1027,8 +1027,8 @@
     1.4  );
     1.5  *}
     1.6  
     1.7 -declaration {* fn _ =>
     1.8 -  Simplifier.map_ss (fn ss => ss
     1.9 +setup {*
    1.10 +  Simplifier.map_simpset_global (fn ss => ss
    1.11      addSolver (mk_solver' "Trancl" (Trancl_Tac.trancl_tac o Simplifier.the_context))
    1.12      addSolver (mk_solver' "Rtrancl" (Trancl_Tac.rtrancl_tac o Simplifier.the_context))
    1.13      addSolver (mk_solver' "Tranclp" (Tranclp_Tac.trancl_tac o Simplifier.the_context))