src/HOL/HOL.thy
changeset 36936 c52d1c130898
parent 36768 46be86127972
child 36945 9bec62c10714
--- a/src/HOL/HOL.thy	Sat May 15 15:31:33 2010 +0200
+++ b/src/HOL/HOL.thy	Sat May 15 17:59:06 2010 +0200
@@ -29,7 +29,6 @@
   "~~/src/Tools/induct.ML"
   ("~~/src/Tools/induct_tacs.ML")
   ("Tools/recfun_codegen.ML")
-  "~~/src/Tools/more_conv.ML"
 begin
 
 setup {* Intuitionistic.method_setup @{binding iprover} *}