equal
deleted
inserted
replaced
738 ; |
738 ; |
739 @@{attribute OF} @{syntax thmrefs} |
739 @@{attribute OF} @{syntax thmrefs} |
740 ; |
740 ; |
741 @@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})? @{syntax for_fixes} |
741 @@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})? @{syntax for_fixes} |
742 ; |
742 ; |
743 @@{attribute "where"} |
743 @@{attribute "where"} @{syntax named_insts} @{syntax for_fixes} |
744 ((@{syntax name} | @{syntax var} | @{syntax typefree} | @{syntax typevar}) '=' |
|
745 (@{syntax type} | @{syntax term}) * @'and') \<newline> @{syntax for_fixes} |
|
746 \<close>} |
744 \<close>} |
747 |
745 |
748 \begin{description} |
746 \begin{description} |
749 |
747 |
750 \item @{command "print_rules"} prints rules declared via attributes |
748 \item @{command "print_rules"} prints rules declared via attributes |