equal
deleted
inserted
replaced
628 ('theorem' | 'lemma') goal |
628 ('theorem' | 'lemma') goal |
629 ; |
629 ; |
630 ('have' | 'show' | 'hence' | 'thus') goal |
630 ('have' | 'show' | 'hence' | 'thus') goal |
631 ; |
631 ; |
632 |
632 |
633 goal: thmdecl? proppat comment? |
633 goal: thmdecl? prop proppat? comment? |
634 ; |
634 ; |
635 \end{rail} |
635 \end{rail} |
636 |
636 |
637 \begin{descr} |
637 \begin{descr} |
638 \item [$\THEOREM{a}{\phi}$] enters proof mode with $\phi$ as main goal, |
638 \item [$\THEOREM{a}{\phi}$] enters proof mode with $\phi$ as main goal, |