equal
deleted
inserted
replaced
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 |