equal
deleted
inserted
replaced
782 \item [@{command "apply_end"}~@{text "m"}] applies proof method |
782 \item [@{command "apply_end"}~@{text "m"}] applies proof method |
783 @{text m} as if in terminal position. Basically, this simulates a |
783 @{text m} as if in terminal position. Basically, this simulates a |
784 multi-step tactic script for @{command "qed"}, but may be given |
784 multi-step tactic script for @{command "qed"}, but may be given |
785 anywhere within the proof body. |
785 anywhere within the proof body. |
786 |
786 |
787 No facts are passed to @{method m} here. Furthermore, the static |
787 No facts are passed to @{text m} here. Furthermore, the static |
788 context is that of the enclosing goal (as for actual @{command |
788 context is that of the enclosing goal (as for actual @{command |
789 "qed"}). Thus the proof method may not refer to any assumptions |
789 "qed"}). Thus the proof method may not refer to any assumptions |
790 introduced in the current body, for example. |
790 introduced in the current body, for example. |
791 |
791 |
792 \item [@{command "done"}] completes a proof script, provided that |
792 \item [@{command "done"}] completes a proof script, provided that |
1018 current context. |
1018 current context. |
1019 |
1019 |
1020 \item [@{attribute trans}] declares theorems as transitivity rules. |
1020 \item [@{attribute trans}] declares theorems as transitivity rules. |
1021 |
1021 |
1022 \item [@{attribute sym}] declares symmetry rules, as well as |
1022 \item [@{attribute sym}] declares symmetry rules, as well as |
1023 @{attribute "Pure.elim?"} rules. |
1023 @{attribute "Pure.elim"}@{text "?"} rules. |
1024 |
1024 |
1025 \item [@{attribute symmetric}] resolves a theorem with some rule |
1025 \item [@{attribute symmetric}] resolves a theorem with some rule |
1026 declared as @{attribute sym} in the current context. For example, |
1026 declared as @{attribute sym} in the current context. For example, |
1027 ``@{command "assume"}~@{text "[symmetric]: x = y"}'' produces a |
1027 ``@{command "assume"}~@{text "[symmetric]: x = y"}'' produces a |
1028 swapped fact derived from that assumption. |
1028 swapped fact derived from that assumption. |