441 |
441 |
442 (*************************************************************************) |
442 (*************************************************************************) |
443 (******************************** Parsers ********************************) |
443 (******************************** Parsers ********************************) |
444 (*************************************************************************) |
444 (*************************************************************************) |
445 |
445 |
446 local structure P = OuterParse and K = OuterKeyword in |
446 val _ = |
447 |
447 Outer_Syntax.local_theory "fixrec" "define recursive functions (HOLCF)" Keyword.thy_decl |
448 val _ = OuterSyntax.local_theory "fixrec" "define recursive functions (HOLCF)" K.thy_decl |
448 ((Parse.opt_keyword "permissive" >> not) -- Parse.fixes -- Parse_Spec.where_alt_specs |
449 ((P.opt_keyword "permissive" >> not) -- P.fixes -- Parse_Spec.where_alt_specs |
449 >> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs)); |
450 >> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs)); |
450 |
451 |
451 val _ = |
452 val _ = OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl |
452 Outer_Syntax.command "fixpat" "define rewrites for fixrec functions" Keyword.thy_decl |
453 (Parse_Spec.specs >> (Toplevel.theory o add_fixpat_cmd)); |
453 (Parse_Spec.specs >> (Toplevel.theory o add_fixpat_cmd)); |
454 |
|
455 end; |
|
456 |
454 |
457 val setup = |
455 val setup = |
458 Attrib.setup @{binding fixrec_simp} |
456 Attrib.setup @{binding fixrec_simp} |
459 (Attrib.add_del fixrec_simp_add fixrec_simp_del) |
457 (Attrib.add_del fixrec_simp_add fixrec_simp_del) |
460 "declaration of fixrec simp rule" |
458 "declaration of fixrec simp rule" |