equal
deleted
inserted
replaced
567 |
567 |
568 val setup = |
568 val setup = |
569 trfun_setup #> |
569 trfun_setup #> |
570 trfun_setup' #> |
570 trfun_setup' #> |
571 term_check_setup #> |
571 term_check_setup #> |
572 term_uncheck_setup; |
572 term_uncheck_setup #> |
|
573 Attrib.setup @{binding case_translation} |
|
574 (Args.term -- Scan.repeat1 Args.term >> |
|
575 (fn (t, ts) => Thm.declaration_attribute (K (register t ts)))) |
|
576 "declaration of case combinators and constructors"; |
573 |
577 |
574 |
578 |
575 (* outer syntax commands *) |
579 (* outer syntax commands *) |
576 |
580 |
577 fun print_case_translations ctxt = |
581 fun print_case_translations ctxt = |