src/HOL/Tools/recdef_package.ML
changeset 24867 e5b55d7be9bb
parent 24712 64ed05609568
child 24927 48e08f37ce92
     1.1 --- a/src/HOL/Tools/recdef_package.ML	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -295,6 +295,8 @@
     1.4  
     1.5  local structure P = OuterParse and K = OuterKeyword in
     1.6  
     1.7 +val _ = OuterSyntax.keywords ["permissive", "congs", "hints"];
     1.8 +
     1.9  val hints =
    1.10    P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- P.arguments) --| P.$$$ ")") >> Args.src;
    1.11  
    1.12 @@ -303,7 +305,7 @@
    1.13    P.name -- P.term -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop) -- Scan.option hints
    1.14    >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
    1.15  
    1.16 -val recdefP =
    1.17 +val _ =
    1.18    OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl
    1.19      (recdef_decl >> Toplevel.theory);
    1.20  
    1.21 @@ -313,21 +315,17 @@
    1.22    Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (SpecParse.xthms1 --| P.$$$ ")")) []
    1.23    >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
    1.24  
    1.25 -val defer_recdefP =
    1.26 +val _ =
    1.27    OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" K.thy_decl
    1.28      (defer_recdef_decl >> Toplevel.theory);
    1.29  
    1.30 -val recdef_tcP =
    1.31 +val _ =
    1.32    OuterSyntax.command "recdef_tc" "recommence proof of termination condition (TFL)" K.thy_goal
    1.33      (P.opt_target --
    1.34        SpecParse.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
    1.35        >> (fn (((loc, thm_name), name), i) =>
    1.36          Toplevel.print o Toplevel.local_theory_to_proof' loc (recdef_tc thm_name name i)));
    1.37  
    1.38 -
    1.39 -val _ = OuterSyntax.add_keywords ["permissive", "congs", "hints"];
    1.40 -val _ = OuterSyntax.add_parsers [recdefP, defer_recdefP, recdef_tcP];
    1.41 -
    1.42  end;
    1.43  
    1.44  end;