src/HOL/Fun_Def.thy
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 *}