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} *}