equal
deleted
inserted
replaced
922 \NEXT & : & \isartrans{proof(state)}{proof(state)} \\ |
922 \NEXT & : & \isartrans{proof(state)}{proof(state)} \\ |
923 \BG & : & \isartrans{proof(state)}{proof(state)} \\ |
923 \BG & : & \isartrans{proof(state)}{proof(state)} \\ |
924 \EN & : & \isartrans{proof(state)}{proof(state)} \\ |
924 \EN & : & \isartrans{proof(state)}{proof(state)} \\ |
925 \end{matharray} |
925 \end{matharray} |
926 |
926 |
|
927 \railalias{lbrace}{\ttlbrace} |
|
928 \railterm{lbrace} |
|
929 |
|
930 \railalias{rbrace}{\ttrbrace} |
|
931 \railterm{rbrace} |
|
932 |
|
933 \begin{rail} |
|
934 'next' comment? |
|
935 ; |
|
936 lbrace comment? |
|
937 ; |
|
938 rbrace comment? |
|
939 ; |
|
940 \end{rail} |
|
941 |
927 While Isar is inherently block-structured, opening and closing blocks is |
942 While Isar is inherently block-structured, opening and closing blocks is |
928 mostly handled rather casually, with little explicit user-intervention. Any |
943 mostly handled rather casually, with little explicit user-intervention. Any |
929 local goal statement automatically opens \emph{two} blocks, which are closed |
944 local goal statement automatically opens \emph{two} blocks, which are closed |
930 again when concluding the sub-proof (by $\QEDNAME$ etc.). Sections of |
945 again when concluding the sub-proof (by $\QEDNAME$ etc.). Sections of |
931 different context within a sub-proof may be switched via $\NEXT$, which is |
946 different context within a sub-proof may be switched via $\NEXT$, which is |