src/HOL/FunDef.thy
changeset 25567 5720345ea689
parent 25556 8d3b7c27049b
child 26748 4d51ddd6aa5c
     1.1 --- a/src/HOL/FunDef.thy	Fri Dec 07 08:38:50 2007 +0100
     1.2 +++ b/src/HOL/FunDef.thy	Fri Dec 07 09:42:20 2007 +0100
     1.3 @@ -18,6 +18,7 @@
     1.4    ("Tools/function_package/pattern_split.ML")
     1.5    ("Tools/function_package/fundef_package.ML")
     1.6    ("Tools/function_package/auto_term.ML")
     1.7 +  ("Tools/function_package/induction_scheme.ML")
     1.8  begin
     1.9  
    1.10  text {* Definitions with default value. *}
    1.11 @@ -104,8 +105,12 @@
    1.12  use "Tools/function_package/pattern_split.ML"
    1.13  use "Tools/function_package/auto_term.ML"
    1.14  use "Tools/function_package/fundef_package.ML"
    1.15 +use "Tools/function_package/induction_scheme.ML"
    1.16  
    1.17 -setup {* FundefPackage.setup *}
    1.18 +setup {* 
    1.19 +  FundefPackage.setup 
    1.20 +  #> InductionScheme.setup
    1.21 +*}
    1.22  
    1.23  lemma let_cong [fundef_cong]:
    1.24    "M = N \<Longrightarrow> (\<And>x. x = N \<Longrightarrow> f x = g x) \<Longrightarrow> Let M f = Let N g"