src/HOL/HOL.thy
changeset 27326 d3beec370964
parent 27212 3a3686dd4433
child 27338 2cd6c60cc10b
--- a/src/HOL/HOL.thy	Mon Jun 23 15:51:37 2008 +0200
+++ b/src/HOL/HOL.thy	Mon Jun 23 15:51:38 2008 +0200
@@ -25,7 +25,7 @@
   "~~/src/Tools/random_word.ML"
   "~~/src/Tools/atomize_elim.ML"
   "~~/src/Tools/induct.ML"
-  ("~~/src/HOL/Tools/induct_tacs.ML")
+  ("~~/src/Tools/induct_tacs.ML")
   "~~/src/Tools/code/code_name.ML"
   "~~/src/Tools/code/code_funcgr.ML"
   "~~/src/Tools/code/code_thingol.ML"
@@ -1554,7 +1554,7 @@
 
 setup Induct.setup
 
-use "~~/src/HOL/Tools/induct_tacs.ML"
+use "~~/src/Tools/induct_tacs.ML"
 setup InductTacs.setup