134 val setup = [RecdefData.init]; |
134 val setup = [RecdefData.init]; |
135 |
135 |
136 |
136 |
137 (* outer syntax *) |
137 (* outer syntax *) |
138 |
138 |
139 local open OuterParse in |
139 local structure P = OuterParse and K = OuterSyntax.Keyword in |
140 |
140 |
141 val recdef_decl = |
141 val recdef_decl = |
142 name -- term -- Scan.repeat1 term -- |
142 P.name -- P.term -- Scan.repeat1 P.term -- |
143 Scan.optional ($$$ "(" |-- $$$ "congs" |-- !!! (xthms1 --| $$$ ")")) [] -- |
143 Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (P.xthms1 --| P.$$$ ")")) [] -- |
144 Scan.option ($$$ "(" |-- $$$ "simpset" |-- !!! (name --| $$$ ")")) |
144 Scan.option (P.$$$ "(" |-- P.$$$ "simpset" |-- P.!!! (P.name --| P.$$$ ")")) |
145 >> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef_x f R eqs ss congs); |
145 >> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef_x f R eqs ss congs); |
146 |
146 |
147 val recdefP = |
147 val recdefP = |
148 OuterSyntax.command "recdef" "define general recursive functions (TFL)" |
148 OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl |
149 (recdef_decl >> Toplevel.theory); |
149 (recdef_decl >> Toplevel.theory); |
150 |
150 |
151 |
151 |
152 val defer_recdef_decl = |
152 val defer_recdef_decl = |
153 name -- Scan.repeat1 term -- |
153 P.name -- Scan.repeat1 P.term -- |
154 Scan.optional ($$$ "(" |-- $$$ "congs" |-- !!! (xthms1 --| $$$ ")")) [] |
154 Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (P.xthms1 --| P.$$$ ")")) [] |
155 >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs); |
155 >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs); |
156 |
156 |
157 val defer_recdefP = |
157 val defer_recdefP = |
158 OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" |
158 OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" K.thy_decl |
159 (defer_recdef_decl >> Toplevel.theory); |
159 (defer_recdef_decl >> Toplevel.theory); |
160 |
160 |
161 val _ = OuterSyntax.add_keywords ["congs", "simpset"]; |
161 val _ = OuterSyntax.add_keywords ["congs", "simpset"]; |
162 val _ = OuterSyntax.add_parsers [recdefP, defer_recdefP]; |
162 val _ = OuterSyntax.add_parsers [recdefP, defer_recdefP]; |
163 |
163 |