equal
deleted
inserted
replaced
191 |
191 |
192 (* outer syntax *) |
192 (* outer syntax *) |
193 |
193 |
194 local structure P = OuterParse and K = OuterKeyword in |
194 local structure P = OuterParse and K = OuterKeyword in |
195 |
195 |
196 val _ = OuterSyntax.keywords ["otherwise"]; |
196 val _ = OuterKeyword.keyword "otherwise"; |
197 |
197 |
198 val _ = |
198 val _ = |
199 OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal |
199 OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal |
200 (fundef_parser default_config |
200 (fundef_parser default_config |
201 >> (fn ((config, fixes), (flags, statements)) => add_fundef fixes statements config flags)); |
201 >> (fn ((config, fixes), (flags, statements)) => add_fundef fixes statements config flags)); |