| changeset 32402 | 5731300da417 |
| parent 32176 | 893614e2c35c |
| child 32544 | e129333b9df0 |
--- a/src/HOL/HOL.thy Wed Aug 26 10:48:45 2009 +0200 +++ b/src/HOL/HOL.thy Wed Aug 26 11:40:28 2009 +0200 @@ -29,6 +29,7 @@ "~~/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} *}