--- a/src/HOL/Tools/function_package/fundef_package.ML Wed Oct 18 10:15:39 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML Wed Oct 18 16:13:03 2006 +0200
@@ -32,6 +32,7 @@
structure FundefPackage =
struct
+open FundefLib
open FundefCommon
(*fn (ctxt,s) => Variable.importT_terms (fst (ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) [] [s])) ctxt;*)
@@ -187,12 +188,13 @@
val functionP =
OuterSyntax.command "function" "define general recursive functions" K.thy_goal
- ((config_parser -- P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
+ ((config_parser default_config -- P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
>> (fn (((config, target), fixes), statements) =>
Toplevel.print o
Toplevel.local_theory_to_proof target (add_fundef fixes statements config)));
+
val terminationP =
OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
(P.opt_locale_target -- Scan.option P.name