src/HOL/Tools/function_package/fundef_package.ML
changeset 21051 c49467a9c1e1
parent 21000 54c42dfbcafa
child 21211 5370cfbf3070
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Oct 18 10:15:39 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Oct 18 16:13:03 2006 +0200
     1.3 @@ -32,6 +32,7 @@
     1.4  structure FundefPackage  =
     1.5  struct
     1.6  
     1.7 +open FundefLib
     1.8  open FundefCommon
     1.9  
    1.10  (*fn (ctxt,s) => Variable.importT_terms (fst (ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) [] [s])) ctxt;*)
    1.11 @@ -187,12 +188,13 @@
    1.12  
    1.13  val functionP =
    1.14    OuterSyntax.command "function" "define general recursive functions" K.thy_goal
    1.15 -  ((config_parser -- P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
    1.16 +  ((config_parser default_config -- P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
    1.17       >> (fn (((config, target), fixes), statements) =>
    1.18              Toplevel.print o
    1.19              Toplevel.local_theory_to_proof target (add_fundef fixes statements config)));
    1.20  
    1.21  
    1.22 +
    1.23  val terminationP =
    1.24    OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
    1.25    (P.opt_locale_target -- Scan.option P.name