src/HOL/Transitive_Closure.thy
changeset 17876 b9c92f384109
parent 17589 58eeffd73be1
child 18372 2bffdf62fe7f
     1.1 --- a/src/HOL/Transitive_Closure.thy	Mon Oct 17 23:10:10 2005 +0200
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Oct 17 23:10:13 2005 +0200
     1.3 @@ -489,9 +489,9 @@
     1.4    
     1.5    end); (* struct *)
     1.6  
     1.7 -simpset_ref() := simpset ()
     1.8 -    addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac))
     1.9 -    addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac));
    1.10 +change_simpset (fn ss => ss
    1.11 +  addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac))
    1.12 +  addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac)));
    1.13  
    1.14  *}
    1.15