1640 \rail@nont{\hyperlink{syntax.axmdecl}{\mbox{\isa{axmdecl}}}}[] |
1640 \rail@nont{\hyperlink{syntax.axmdecl}{\mbox{\isa{axmdecl}}}}[] |
1641 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[] |
1641 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[] |
1642 \rail@nextplus{1} |
1642 \rail@nextplus{1} |
1643 \rail@endplus |
1643 \rail@endplus |
1644 \rail@end |
1644 \rail@end |
1645 \rail@begin{3}{} |
1645 \rail@begin{6}{} |
1646 \rail@bar |
1646 \rail@bar |
1647 \rail@term{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}}[] |
1647 \rail@term{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}}[] |
1648 \rail@nextbar{1} |
1648 \rail@nextbar{1} |
1649 \rail@term{\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}}[] |
1649 \rail@term{\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}}[] |
1650 \rail@endbar |
1650 \rail@endbar |
1651 \rail@bar |
1651 \rail@bar |
1652 \rail@nextbar{1} |
1652 \rail@nextbar{1} |
1653 \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[] |
1653 \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[] |
1654 \rail@endbar |
1654 \rail@endbar |
1655 \rail@plus |
1655 \rail@cr{3} |
1656 \rail@bar |
1656 \rail@plus |
1657 \rail@nextbar{1} |
1657 \rail@bar |
|
1658 \rail@nextbar{4} |
1658 \rail@nont{\hyperlink{syntax.thmdef}{\mbox{\isa{thmdef}}}}[] |
1659 \rail@nont{\hyperlink{syntax.thmdef}{\mbox{\isa{thmdef}}}}[] |
1659 \rail@endbar |
1660 \rail@endbar |
1660 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[] |
1661 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[] |
1661 \rail@nextplus{2} |
1662 \rail@nextplus{5} |
1662 \rail@cterm{\isa{\isakeyword{and}}}[] |
1663 \rail@cterm{\isa{\isakeyword{and}}}[] |
1663 \rail@endplus |
1664 \rail@endplus |
|
1665 \rail@bar |
|
1666 \rail@nextbar{4} |
|
1667 \rail@term{\isa{\isakeyword{for}}}[] |
|
1668 \rail@plus |
|
1669 \rail@nont{\hyperlink{syntax.vars}{\mbox{\isa{vars}}}}[] |
|
1670 \rail@nextplus{5} |
|
1671 \rail@cterm{\isa{\isakeyword{and}}}[] |
|
1672 \rail@endplus |
|
1673 \rail@endbar |
1664 \rail@end |
1674 \rail@end |
1665 \end{railoutput} |
1675 \end{railoutput} |
1666 |
1676 |
1667 |
1677 |
1668 \begin{description} |
1678 \begin{description} |
1674 |
1684 |
1675 Axioms are usually only introduced when declaring new logical |
1685 Axioms are usually only introduced when declaring new logical |
1676 systems. Everyday work is typically done the hard way, with proper |
1686 systems. Everyday work is typically done the hard way, with proper |
1677 definitions and proven theorems. |
1687 definitions and proven theorems. |
1678 |
1688 |
1679 \item \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isaliteral{3D}{\isacharequal}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} retrieves and stores |
1689 \item \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isaliteral{3D}{\isacharequal}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}~\indexdef{}{keyword}{for}\hypertarget{keyword.for}{\hyperlink{keyword.for}{\mbox{\isa{\isakeyword{for}}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}} evaluates given facts (with attributes) in |
1680 existing facts in the theory context, or the specified target |
1690 the current context, which may be augmented by local variables. |
1681 context (see also \secref{sec:target}). Typical applications would |
1691 Results are standardized before being stored, i.e.\ schematic |
1682 also involve attributes, to declare Simplifier rules, for example. |
1692 variables are renamed to enforce index \isa{{\isaliteral{22}{\isachardoublequote}}{\isadigit{0}}{\isaliteral{22}{\isachardoublequote}}} uniformly. |
1683 |
1693 |
1684 \item \hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}} is essentially the same as \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}, but marks the result as a different kind of facts. |
1694 \item \hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}} is the same as \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}, but |
|
1695 marks the result as a different kind of facts. |
1685 |
1696 |
1686 \end{description}% |
1697 \end{description}% |
1687 \end{isamarkuptext}% |
1698 \end{isamarkuptext}% |
1688 \isamarkuptrue% |
1699 \isamarkuptrue% |
1689 % |
1700 % |