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

author | wenzelm |

Tue, 14 Mar 2000 11:31:45 +0100 | |

changeset 8448 | e7df316491d4 |

parent 8447 | 1181723cf835 |

child 8449 | f8ff23736465 |

tuned 'case';

--- a/doc-src/IsarRef/pure.tex Tue Mar 14 11:31:04 2000 +0100 +++ b/doc-src/IsarRef/pure.tex Tue Mar 14 11:31:45 2000 +0100 @@ -528,8 +528,8 @@ at the current goal state, which is considered strictly non-observable in Isar. Instead, the cases considered here typically emerge in a canonical way from certain pieces of specification that appears in the theory somewhere, -such as an inductive definition, or recursive function. See \S\ref{sec:FIXME} -for more details of how this works in HOL. +such as an inductive definition, or recursive function. See +\S\ref{sec:induct-method} for more details of how this works in HOL. \begin{rail} 'fix' (vars + 'and') comment? @@ -538,7 +538,7 @@ ; 'def' thmdecl? \\ var '==' term termpat? comment? ; - 'case' name + 'case' name attributes? ; var: name ('::' type)? @@ -822,7 +822,7 @@ \indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}} \begin{matharray}{rcl} - \isarcmd{next} & : & \isartrans{proof(state)}{proof(state)} \\ + \NEXT & : & \isartrans{proof(state)}{proof(state)} \\ \BG & : & \isartrans{proof(state)}{proof(state)} \\ \EN & : & \isartrans{proof(state)}{proof(state)} \\ \end{matharray} @@ -831,17 +831,17 @@ mostly handled rather casually, with little explicit user-intervention. Any local goal statement automatically opens \emph{two} blocks, which are closed again when concluding the sub-proof (by $\QEDNAME$ etc.). Sections of -different context within a sub-proof may be switched via $\isarkeyword{next}$, -which is just a single block-close followed by block-open again. Thus the -effect of $\isarkeyword{next}$ to reset the local proof context. There is no -goal focus involved here! +different context within a sub-proof may be switched via $\NEXT$, which is +just a single block-close followed by block-open again. Thus the effect of +$\NEXT$ to reset the local proof context. There is no goal focus involved +here! For slightly more advanced applications, there are explicit block parentheses as well. These typically achieve a stronger forward style of reasoning. \begin{descr} -\item [$\isarkeyword{next}$] switches to a fresh block within a sub-proof, - resetting the local context to the initial one. +\item [$\NEXT$] switches to a fresh block within a sub-proof, resetting the + local context to the initial one. \item [$\isarkeyword{\{\{}$ and $\isarkeyword{\}\}}$] explicitly open and close blocks. Any current facts pass through ``$\isarkeyword{\{\{}$'' unchanged, while ``$\isarkeyword{\}\}}$'' causes any result to be @@ -855,7 +855,7 @@ \section{Other commands} -\subsection{Diagnostics} +\subsection{Diagnostics}\label{sec:diag} \indexisarcmd{thm}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{typ} \indexisarcmd{print-facts}\indexisarcmd{print-binds}\indexisarcmd{print-cases}