src/HOL/Tools/recdef_package.ML
changeset 9652 ea1f02d6d65b
parent 9640 8c6cf4f01644
child 9859 2cd338998b53
equal deleted inserted replaced
9651:f0cfddda6038 9652:ea1f02d6d65b
   102       |> put_recdef name result
   102       |> put_recdef name result
   103       |> Theory.parent_path;
   103       |> Theory.parent_path;
   104   in (thy, result) end;
   104   in (thy, result) end;
   105 
   105 
   106 val add_recdef = gen_add_recdef Tfl.define Attrib.global_attribute IsarThy.apply_theorems;
   106 val add_recdef = gen_add_recdef Tfl.define Attrib.global_attribute IsarThy.apply_theorems;
   107 val add_recdef_x = gen_add_recdef Tfl.define Attrib.global_attribute IsarThy.apply_theorems;
       
   108 val add_recdef_i = gen_add_recdef Tfl.define_i (K I) IsarThy.apply_theorems_i;
   107 val add_recdef_i = gen_add_recdef Tfl.define_i (K I) IsarThy.apply_theorems_i;
   109 
   108 
   110 
   109 
   111 
   110 
   112 (** defer_recdef(_i) **)
   111 (** defer_recdef(_i) **)
   145 local structure P = OuterParse and K = OuterSyntax.Keyword in
   144 local structure P = OuterParse and K = OuterSyntax.Keyword in
   146 
   145 
   147 val recdef_decl =
   146 val recdef_decl =
   148   P.name -- P.term -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment) --
   147   P.name -- P.term -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment) --
   149   Scan.optional (P.$$$ "congs" |-- P.!!! P.xthms1) []
   148   Scan.optional (P.$$$ "congs" |-- P.!!! P.xthms1) []
   150   >> (fn (((f, R), eqs), congs) => #1 o add_recdef_x f R (map P.triple_swap eqs) None congs);
   149   >> (fn (((f, R), eqs), congs) => #1 o add_recdef f R (map P.triple_swap eqs) None congs);
   151 
   150 
   152 val recdefP =
   151 val recdefP =
   153   OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl
   152   OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl
   154     (recdef_decl >> Toplevel.theory);
   153     (recdef_decl >> Toplevel.theory);
   155 
   154