src/HOL/HOL.thy
changeset 27326 d3beec370964
parent 27212 3a3686dd4433
child 27338 2cd6c60cc10b
     1.1 --- a/src/HOL/HOL.thy	Mon Jun 23 15:51:37 2008 +0200
     1.2 +++ b/src/HOL/HOL.thy	Mon Jun 23 15:51:38 2008 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4    "~~/src/Tools/random_word.ML"
     1.5    "~~/src/Tools/atomize_elim.ML"
     1.6    "~~/src/Tools/induct.ML"
     1.7 -  ("~~/src/HOL/Tools/induct_tacs.ML")
     1.8 +  ("~~/src/Tools/induct_tacs.ML")
     1.9    "~~/src/Tools/code/code_name.ML"
    1.10    "~~/src/Tools/code/code_funcgr.ML"
    1.11    "~~/src/Tools/code/code_thingol.ML"
    1.12 @@ -1554,7 +1554,7 @@
    1.13  
    1.14  setup Induct.setup
    1.15  
    1.16 -use "~~/src/HOL/Tools/induct_tacs.ML"
    1.17 +use "~~/src/Tools/induct_tacs.ML"
    1.18  setup InductTacs.setup
    1.19  
    1.20