changeset 58826 | 2ed2eaabe3df |
parent 58819 | aa43c6f05bca |
child 58889 | 5b7a9633cfa8 |
--- a/src/HOL/Fun_Def.thy Wed Oct 29 17:01:44 2014 +0100 +++ b/src/HOL/Fun_Def.thy Wed Oct 29 19:01:49 2014 +0100 @@ -106,11 +106,6 @@ Scan.succeed (NO_CASES oo Induction_Schema.induction_schema_tac) *} "prove an induction principle" -setup {* - Function.setup - #> Function_Fun.setup -*} - subsection {* Measure functions *}