summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Mon, 30 Aug 1999 20:30:39 +0200 | |

changeset 7397 | 9228085a25df |

parent 7396 | d3f231fe725c |

child 7398 | c68ecbf05eb6 |

tuned;

--- a/doc-src/IsarRef/pure.tex Mon Aug 30 20:30:21 1999 +0200 +++ b/doc-src/IsarRef/pure.tex Mon Aug 30 20:30:39 1999 +0200 @@ -769,6 +769,13 @@ \subsection{Block structure} +\indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}} +\begin{matharray}{rcl} + \isarcmd{next} & : & \isartrans{proof(state)}{proof(state)} \\ + \isarcmd{\{\{} & : & \isartrans{proof(state)}{proof(state)} \\ + \isarcmd{\}\}} & : & \isartrans{proof(state)}{proof(state)} \\ +\end{matharray} + While Isar is inherently block-structured, opening and closing blocks is mostly handled rather casually, with little explicit user-intervention. Any local goal statement automatically opens \emph{two} blocks, which are closed @@ -782,13 +789,6 @@ For slightly more advanced applications, there are explicit block parentheses as well. These typically achieve a strong forward style of reasoning. -\indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}} -\begin{matharray}{rcl} - \isarcmd{next} & : & \isartrans{proof(state)}{proof(state)} \\ - \isarcmd{\{\{} & : & \isartrans{proof(state)}{proof(state)} \\ - \isarcmd{\}\}} & : & \isartrans{proof(state)}{proof(state)} \\ -\end{matharray} - \begin{descr} \item [$\isarkeyword{next}$] switches to a fresh block within a sub-proof, resetting the context to the initial one. @@ -861,8 +861,8 @@ $\isarkeyword{update_thy}$, and $\isarkeyword{update_thy_only}$] load some theory given as $name$ argument. These commands are exactly the same as the corresponding ML functions (see also \cite[\S1,\S6]{isabelle-ref}). Note - that both the ML and Isar versions of these commands may load new- and - old-style theories alike. + that both the ML and Isar versions may load new- and old-style theories + alike. \end{descr} Note that these system commands are scarcely used when working with