equal
deleted
inserted
replaced
594 \rail@nextbar{1} |
594 \rail@nextbar{1} |
595 \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[] |
595 \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[] |
596 \rail@endbar |
596 \rail@endbar |
597 \rail@plus |
597 \rail@plus |
598 \rail@nextplus{1} |
598 \rail@nextplus{1} |
599 \rail@cnont{\hyperlink{syntax.contextelem}{\mbox{\isa{contextelem}}}}[] |
599 \rail@cnont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[] |
600 \rail@endplus |
600 \rail@endplus |
601 \rail@nont{\isa{conclusion}}[] |
601 \rail@nont{\isa{conclusion}}[] |
602 \rail@end |
602 \rail@end |
603 \rail@begin{4}{\isa{conclusion}} |
603 \rail@begin{4}{\isa{conclusion}} |
604 \rail@bar |
604 \rail@bar |
636 \begin{description} |
636 \begin{description} |
637 |
637 |
638 \item \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} enters proof mode with |
638 \item \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} enters proof mode with |
639 \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} as main goal, eventually resulting in some fact \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} to be put back into the target context. An additional \hyperlink{syntax.context}{\mbox{\isa{context}}} specification may build up an initial proof context for the |
639 \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} as main goal, eventually resulting in some fact \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} to be put back into the target context. An additional \hyperlink{syntax.context}{\mbox{\isa{context}}} specification may build up an initial proof context for the |
640 subsequent claim; this includes local definitions and syntax as |
640 subsequent claim; this includes local definitions and syntax as |
641 well, see the definition of \hyperlink{syntax.contextelem}{\mbox{\isa{contextelem}}} in |
641 well, see the definition of \hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}} in |
642 \secref{sec:locale}. |
642 \secref{sec:locale}. |
643 |
643 |
644 \item \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} and \hyperlink{command.corollary}{\mbox{\isa{\isacommand{corollary}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} are essentially the same as \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}}, but the facts are internally marked as |
644 \item \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} and \hyperlink{command.corollary}{\mbox{\isa{\isacommand{corollary}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} are essentially the same as \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}}, but the facts are internally marked as |
645 being of a different kind. This discrimination acts like a formal |
645 being of a different kind. This discrimination acts like a formal |
646 comment. |
646 comment. |
1751 \rail@nont{\isa{rule}}[] |
1751 \rail@nont{\isa{rule}}[] |
1752 \rail@endbar |
1752 \rail@endbar |
1753 \rail@end |
1753 \rail@end |
1754 \rail@begin{2}{\isa{}} |
1754 \rail@begin{2}{\isa{}} |
1755 \rail@term{\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}}[] |
1755 \rail@term{\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}}[] |
1756 \rail@nont{\isa{insts}}[] |
1756 \rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[] |
1757 \rail@nont{\isa{taking}}[] |
1757 \rail@nont{\isa{taking}}[] |
1758 \rail@bar |
1758 \rail@bar |
1759 \rail@nextbar{1} |
1759 \rail@nextbar{1} |
1760 \rail@nont{\isa{rule}}[] |
1760 \rail@nont{\isa{rule}}[] |
1761 \rail@endbar |
1761 \rail@endbar |
1819 \rail@endplus |
1819 \rail@endplus |
1820 \rail@end |
1820 \rail@end |
1821 \rail@begin{1}{\isa{taking}} |
1821 \rail@begin{1}{\isa{taking}} |
1822 \rail@term{\isa{taking}}[] |
1822 \rail@term{\isa{taking}}[] |
1823 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[] |
1823 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[] |
1824 \rail@nont{\isa{insts}}[] |
1824 \rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[] |
1825 \rail@end |
1825 \rail@end |
1826 \end{railoutput} |
1826 \end{railoutput} |
1827 |
1827 |
1828 |
1828 |
1829 \begin{description} |
1829 \begin{description} |