author  wenzelm 
Fri, 10 Nov 2000 19:02:37 +0100  
changeset 10432  3dfbc913d184 
parent 10223  31346d22bb54 
child 10550  93ca45370c59 
permissions  rwrr 
7046  1 

7895  2 
\chapter{Basic Isar Language Elements}\label{ch:puresyntax} 
7167  3 

8515  4 
Subsequently, we introduce the main part of Pure Isar theory and proof 
8547  5 
commands, together with fundamental proof methods and attributes. 
8515  6 
Chapter~\ref{ch:gentools} describes further Isar elements provided by generic 
7 
tools and packages (such as the Simplifier) that are either part of Pure 

8 
Isabelle or preinstalled by most object logics. Chapter~\ref{ch:holtools} 

9 
refers to actual objectlogic specific elements of Isabelle/HOL. 

7046  10 

7167  11 
\medskip 
12 

13 
Isar commands may be either \emph{proper} document constructors, or 

7466  14 
\emph{improper commands}. Some proof methods and attributes introduced later 
15 
are classified as improper as well. Improper Isar language elements, which 

16 
are subsequently marked by $^*$, are often helpful when developing proof 

7981  17 
documents, while their use is discouraged for the final outcome. Typical 
18 
examples are diagnostic commands that print terms or theorems according to the 

19 
current context; other commands even emulate oldstyle tactical theorem 

8547  20 
proving. 
7167  21 

7134  22 

23 
\section{Theory commands} 

24 

7167  25 
\subsection{Defining theories}\label{sec:beginthy} 
7134  26 

7895  27 
\indexisarcmd{header}\indexisarcmd{theory}\indexisarcmd{end}\indexisarcmd{context} 
7134  28 
\begin{matharray}{rcl} 
7895  29 
\isarcmd{header} & : & \isarkeep{toplevel} \\ 
8510  30 
\isarcmd{theory} & : & \isartrans{toplevel}{theory} \\ 
31 
\isarcmd{context}^* & : & \isartrans{toplevel}{theory} \\ 

32 
\isarcmd{end} & : & \isartrans{theory}{toplevel} \\ 

7134  33 
\end{matharray} 
34 

35 
Isabelle/Isar ``newstyle'' theories are either defined via theory files or 

7981  36 
interactively. Both theorylevel specifications and proofs are handled 
7335  37 
uniformly  occasionally definitional mechanisms even require some explicit 
38 
proof as well. In contrast, ``oldstyle'' Isabelle theories support batch 

39 
processing only, with the proof scripts collected in separate ML files. 

7134  40 

7895  41 
The first actual command of any theory has to be $\THEORY$, starting a new 
42 
theory based on the merge of existing ones. Just preceding $\THEORY$, there 

43 
may be an optional $\isarkeyword{header}$ declaration, which is relevant to 

44 
document preparation only; it acts very much like a special pretheory markup 

45 
command (cf.\ \S\ref{sec:markupthy} and \S\ref{sec:markupthy}). The theory 

46 
context may be also changed by $\CONTEXT$ without creating a new theory. In 

47 
both cases, $\END$ concludes the theory development; it has to be the very 

8547  48 
last command of any theory file. 
7134  49 

50 
\begin{rail} 

7895  51 
'header' text 
52 
; 

7134  53 
'theory' name '=' (name + '+') filespecs? ':' 
54 
; 

55 
'context' name 

56 
; 

57 
'end' 

58 
;; 

59 

7167  60 
filespecs: 'files' ((name  parname) +); 
7134  61 
\end{rail} 
62 

7167  63 
\begin{descr} 
7895  64 
\item [$\isarkeyword{header}~text$] provides plain text markup just preceding 
8547  65 
the formal beginning of a theory. In actual document preparation the 
7895  66 
corresponding {\LaTeX} macro \verb,\isamarkupheader, may be redefined to 
67 
produce chapter or section headings. See also \S\ref{sec:markupthy} and 

68 
\S\ref{sec:markupprf} for further markup commands. 

69 

7981  70 
\item [$\THEORY~A = B@1 + \cdots + B@n\colon$] commences a new theory $A$ 
71 
based on existing ones $B@1 + \cdots + B@n$. Isabelle's theory loader 

72 
system ensures that any of the base theories are properly loaded (and fully 

73 
uptodate when $\THEORY$ is executed interactively). The optional 

74 
$\isarkeyword{files}$ specification declares additional dependencies on ML 

75 
files. Unless put in parentheses, any file will be loaded immediately via 

76 
$\isarcmd{use}$ (see also \S\ref{sec:ML}). The optional ML file 

77 
\texttt{$A$.ML} that may be associated with any theory should \emph{not} be 

78 
included in $\isarkeyword{files}$, though. 

7134  79 

7895  80 
\item [$\CONTEXT~B$] enters an existing theory context, basically in readonly 
7981  81 
mode, so only a limited set of commands may be performed without destroying 
82 
the theory. Just as for $\THEORY$, the theory loader ensures that $B$ is 

83 
loaded and uptodate. 

7175  84 

7167  85 
\item [$\END$] concludes the current theory definition or context switch. 
7981  86 
Note that this command cannot be undone, but the whole theory definition has 
87 
to be retracted. 

7167  88 
\end{descr} 
7134  89 

90 

7895  91 
\subsection{Theory markup commands}\label{sec:markupthy} 
7134  92 

7895  93 
\indexisarcmd{chapter}\indexisarcmd{section}\indexisarcmd{subsection} 
94 
\indexisarcmd{subsubsection}\indexisarcmd{text}\indexisarcmd{textraw} 

7134  95 
\begin{matharray}{rcl} 
96 
\isarcmd{chapter} & : & \isartrans{theory}{theory} \\ 

7167  97 
\isarcmd{section} & : & \isartrans{theory}{theory} \\ 
7134  98 
\isarcmd{subsection} & : & \isartrans{theory}{theory} \\ 
99 
\isarcmd{subsubsection} & : & \isartrans{theory}{theory} \\ 

100 
\isarcmd{text} & : & \isartrans{theory}{theory} \\ 

7895  101 
\isarcmd{text_raw} & : & \isartrans{theory}{theory} \\ 
7134  102 
\end{matharray} 
103 

7895  104 
Apart from formal comments (see \S\ref{sec:comments}), markup commands provide 
7981  105 
a structured way to insert text into the document generated from a theory (see 
7895  106 
\cite{isabellesys} for more information on Isabelle's document preparation 
107 
tools). 

7134  108 

7895  109 
\railalias{textraw}{text\_raw} 
110 
\railterm{textraw} 

7134  111 

112 
\begin{rail} 

7895  113 
('chapter'  'section'  'subsection'  'subsubsection'  'text'  textraw) text 
7134  114 
; 
115 
\end{rail} 

116 

7167  117 
\begin{descr} 
7335  118 
\item [$\isarkeyword{chapter}$, $\isarkeyword{section}$, 
119 
$\isarkeyword{subsection}$, and $\isarkeyword{subsubsection}$] mark chapter 

120 
and section headings. 

7895  121 
\item [$\TEXT$] specifies paragraphs of plain text, including references to 
122 
formal entities.\footnote{The latter feature is not yet supported. 

123 
Nevertheless, any source text of the form 

124 
``\texttt{\at\ttlbrace$\dots$\ttrbrace}'' should be considered as reserved 

125 
for future use.} 

126 
\item [$\isarkeyword{text_raw}$] inserts {\LaTeX} source into the output, 

127 
without additional markup. Thus the full range of document manipulations 

128 
becomes available. A typical application would be to emit 

129 
\verb,\begin{comment}, and \verb,\end{comment}, commands to exclude certain 

130 
parts from the final document.\footnote{This requires the \texttt{comment} 

8547  131 
package to be included in {\LaTeX}, of course.} 
7167  132 
\end{descr} 
7134  133 

8684  134 
Any of these markup elements corresponds to a {\LaTeX} command with the name 
135 
prefixed by \verb,\isamarkup,. For the sectioning commands this is a plain 

136 
macro with a single argument, e.g.\ \verb,\isamarkupchapter{,\dots\verb,}, for 

137 
$\isarkeyword{chapter}$. The $\isarkeyword{text}$ markup results in a 

138 
{\LaTeX} environment \verb,\begin{isamarkuptext}, {\dots} 

139 
\verb,\end{isamarkuptext},, while $\isarkeyword{text_raw}$ causes the text 

140 
to be inserted directly into the {\LaTeX} source. 

7895  141 

8485  142 
\medskip 
143 

144 
Additional markup commands are available for proofs (see 

7895  145 
\S\ref{sec:markupprf}). Also note that the $\isarkeyword{header}$ 
8684  146 
declaration (see \S\ref{sec:beginthy}) admits to insert section markup just 
147 
preceding the actual theory definition. 

7895  148 

7134  149 

7135  150 
\subsection{Type classes and sorts}\label{sec:classes} 
7134  151 

152 
\indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort} 

153 
\begin{matharray}{rcl} 

154 
\isarcmd{classes} & : & \isartrans{theory}{theory} \\ 

155 
\isarcmd{classrel} & : & \isartrans{theory}{theory} \\ 

156 
\isarcmd{defaultsort} & : & \isartrans{theory}{theory} \\ 

157 
\end{matharray} 

158 

159 
\begin{rail} 

7167  160 
'classes' (classdecl comment? +) 
7134  161 
; 
162 
'classrel' nameref '<' nameref comment? 

163 
; 

164 
'defaultsort' sort comment? 

165 
; 

166 
\end{rail} 

167 

7167  168 
\begin{descr} 
7335  169 
\item [$\isarkeyword{classes}~c<\vec c$] declares class $c$ to be a subclass 
170 
of existing classes $\vec c$. Cyclic class structures are ruled out. 

7134  171 
\item [$\isarkeyword{classrel}~c@1<c@2$] states a subclass relation between 
172 
existing classes $c@1$ and $c@2$. This is done axiomatically! The 

10223  173 
$\INSTANCE$ command (see \S\ref{sec:axclass}) provides a way to introduce 
174 
proven class relations. 

7134  175 
\item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for 
7895  176 
any type variables given without sort constraints. Usually, the default 
8547  177 
sort would be only changed when defining new objectlogics. 
7167  178 
\end{descr} 
7134  179 

180 

7315  181 
\subsection{Primitive types and type abbreviations}\label{sec:typespure} 
7134  182 

183 
\indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities} 

184 
\begin{matharray}{rcl} 

185 
\isarcmd{types} & : & \isartrans{theory}{theory} \\ 

186 
\isarcmd{typedecl} & : & \isartrans{theory}{theory} \\ 

187 
\isarcmd{nonterminals} & : & \isartrans{theory}{theory} \\ 

188 
\isarcmd{arities} & : & \isartrans{theory}{theory} \\ 

189 
\end{matharray} 

190 

191 
\begin{rail} 

192 
'types' (typespec '=' type infix? comment? +) 

193 
; 

194 
'typedecl' typespec infix? comment? 

195 
; 

196 
'nonterminals' (name +) comment? 

197 
; 

198 
'arities' (nameref '::' arity comment? +) 

199 
; 

200 
\end{rail} 

201 

7167  202 
\begin{descr} 
7335  203 
\item [$\TYPES~(\vec\alpha)t = \tau$] introduces \emph{type synonym} 
7134  204 
$(\vec\alpha)t$ for existing type $\tau$. Unlike actual type definitions, 
205 
as are available in Isabelle/HOL for example, type synonyms are just purely 

7895  206 
syntactic abbreviations without any logical significance. Internally, type 
7981  207 
synonyms are fully expanded. 
7134  208 
\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] declares a new type constructor 
7895  209 
$t$, intended as an actual logical type. Note that objectlogics such as 
210 
Isabelle/HOL override $\isarkeyword{typedecl}$ by their own version. 

7175  211 
\item [$\isarkeyword{nonterminals}~\vec c$] declares $0$ary type constructors 
212 
$\vec c$ to act as purely syntactic types, i.e.\ nonterminal symbols of 

213 
Isabelle's inner syntax of terms or types. 

7335  214 
\item [$\isarkeyword{arities}~t::(\vec s)s$] augments Isabelle's ordersorted 
215 
signature of types by new type constructor arities. This is done 

10223  216 
axiomatically! The $\INSTANCE$ command (see \S\ref{sec:axclass}) provides a 
217 
way to introduce proven type arities. 

7167  218 
\end{descr} 
7134  219 

220 

7981  221 
\subsection{Constants and simple definitions}\label{sec:consts} 
7134  222 

7175  223 
\indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}\indexoutertoken{constdecl} 
7134  224 
\begin{matharray}{rcl} 
225 
\isarcmd{consts} & : & \isartrans{theory}{theory} \\ 

226 
\isarcmd{defs} & : & \isartrans{theory}{theory} \\ 

227 
\isarcmd{constdefs} & : & \isartrans{theory}{theory} \\ 

228 
\end{matharray} 

229 

230 
\begin{rail} 

231 
'consts' (constdecl +) 

232 
; 

9308  233 
'defs' ('(overloaded)')? (axmdecl prop comment? +) 
7134  234 
; 
235 
'constdefs' (constdecl prop comment? +) 

236 
; 

237 

238 
constdecl: name '::' type mixfix? comment? 

239 
; 

240 
\end{rail} 

241 

7167  242 
\begin{descr} 
7335  243 
\item [$\CONSTS~c::\sigma$] declares constant $c$ to have any instance of type 
244 
scheme $\sigma$. The optional mixfix annotations may attach concrete syntax 

7895  245 
to the constants declared. 
9308  246 

7335  247 
\item [$\DEFS~name: eqn$] introduces $eqn$ as a definitional axiom for some 
248 
existing constant. See \cite[\S6]{isabelleref} for more details on the 

249 
form of equations admitted as constant definitions. 

9308  250 

251 
The $overloaded$ option declares definitions to be potentially overloaded. 

252 
Unless this option is given, a warning message would be issued for any 

253 
definitional equation with a more special type than that of the 

254 
corresponding constant declaration. 

255 

7335  256 
\item [$\isarkeyword{constdefs}~c::\sigma~eqn$] combines declarations and 
8547  257 
definitions of constants, using the canonical name $c_def$ for the 
258 
definitional axiom. 

7167  259 
\end{descr} 
7134  260 

261 

7981  262 
\subsection{Syntax and translations}\label{sec:syntrans} 
7134  263 

264 
\indexisarcmd{syntax}\indexisarcmd{translations} 

265 
\begin{matharray}{rcl} 

266 
\isarcmd{syntax} & : & \isartrans{theory}{theory} \\ 

267 
\isarcmd{translations} & : & \isartrans{theory}{theory} \\ 

268 
\end{matharray} 

269 

270 
\begin{rail} 

9727  271 
'syntax' ('(' ( name  'output'  name 'output' ) ')')? (constdecl +) 
7134  272 
; 
273 
'translations' (transpat ('=='  '=>'  '<=') transpat comment? +) 

274 
; 

275 
transpat: ('(' nameref ')')? string 

276 
; 

277 
\end{rail} 

278 

7167  279 
\begin{descr} 
7175  280 
\item [$\isarkeyword{syntax}~(mode)~decls$] is similar to $\CONSTS~decls$, 
281 
except that the actual logical signature extension is omitted. Thus the 

282 
context free grammar of Isabelle's inner syntax may be augmented in 

7335  283 
arbitrary ways, independently of the logic. The $mode$ argument refers to 
8547  284 
the print mode that the grammar rules belong; unless the \texttt{output} 
285 
flag is given, all productions are added both to the input and output 

286 
grammar. 

7175  287 
\item [$\isarkeyword{translations}~rules$] specifies syntactic translation 
7981  288 
rules (i.e.\ \emph{macros}): parse~/ print rules (\texttt{==}), parse rules 
7895  289 
(\texttt{=>}), or print rules (\texttt{<=}). Translation patterns may be 
290 
prefixed by the syntactic category to be used for parsing; the default is 

7134  291 
\texttt{logic}. 
7167  292 
\end{descr} 
7134  293 

294 

9605  295 
\subsection{Axioms and theorems}\label{sec:axmsthms} 
7134  296 

297 
\indexisarcmd{axioms}\indexisarcmd{theorems}\indexisarcmd{lemmas} 

298 
\begin{matharray}{rcl} 

299 
\isarcmd{axioms} & : & \isartrans{theory}{theory} \\ 

300 
\isarcmd{theorems} & : & \isartrans{theory}{theory} \\ 

301 
\isarcmd{lemmas} & : & \isartrans{theory}{theory} \\ 

302 
\end{matharray} 

303 

304 
\begin{rail} 

7135  305 
'axioms' (axmdecl prop comment? +) 
7134  306 
; 
9199  307 
('theorems'  'lemmas') (thmdef? thmrefs comment? + 'and') 
7134  308 
; 
309 
\end{rail} 

310 

7167  311 
\begin{descr} 
7335  312 
\item [$\isarkeyword{axioms}~a: \phi$] introduces arbitrary statements as 
7895  313 
axioms of the metalogic. In fact, axioms are ``axiomatic theorems'', and 
314 
may be referred later just as any other theorem. 

7134  315 

316 
Axioms are usually only introduced when declaring new logical systems. 

7175  317 
Everyday work is typically done the hard way, with proper definitions and 
8547  318 
actual proven theorems. 
7335  319 
\item [$\isarkeyword{theorems}~a = \vec b$] stores lists of existing theorems. 
8547  320 
Typical applications would also involve attributes, to declare Simplifier 
321 
rules, for example. 

7134  322 
\item [$\isarkeyword{lemmas}$] is similar to $\isarkeyword{theorems}$, but 
323 
tags the results as ``lemma''. 

7167  324 
\end{descr} 
7134  325 

326 

7167  327 
\subsection{Name spaces} 
7134  328 

8726  329 
\indexisarcmd{global}\indexisarcmd{local}\indexisarcmd{hide} 
7134  330 
\begin{matharray}{rcl} 
331 
\isarcmd{global} & : & \isartrans{theory}{theory} \\ 

332 
\isarcmd{local} & : & \isartrans{theory}{theory} \\ 

8726  333 
\isarcmd{hide} & : & \isartrans{theory}{theory} \\ 
7134  334 
\end{matharray} 
335 

8726  336 
\begin{rail} 
337 
'global' comment? 

338 
; 

339 
'local' comment? 

340 
; 

341 
'hide' name (nameref + ) comment? 

342 
; 

343 
\end{rail} 

344 

7895  345 
Isabelle organizes any kind of name declarations (of types, constants, 
8547  346 
theorems etc.) by separate hierarchically structured name spaces. Normally 
8726  347 
the user does not have to control the behavior of name spaces by hand, yet the 
348 
following commands provide some way to do so. 

7175  349 

7167  350 
\begin{descr} 
351 
\item [$\isarkeyword{global}$ and $\isarkeyword{local}$] change the current 

352 
name declaration mode. Initially, theories start in $\isarkeyword{local}$ 

353 
mode, causing all names to be automatically qualified by the theory name. 

7895  354 
Changing this to $\isarkeyword{global}$ causes all names to be declared 
355 
without the theory prefix, until $\isarkeyword{local}$ is declared again. 

8726  356 

357 
Note that global names are prone to get hidden accidently later, when 

358 
qualified names of the same base name are introduced. 

359 

360 
\item [$\isarkeyword{hide}~space~names$] removes declarations from a given 

361 
name space (which may be $class$, $type$, or $const$). Hidden objects 

362 
remain valid within the logic, but are inaccessible from user input. In 

363 
output, the special qualifier ``$\mathord?\mathord?$'' is prefixed to the 

364 
full internal name. 

365 

366 
Unqualified (global) names may not be hidden deliberately. 

7167  367 
\end{descr} 
7134  368 

369 

7167  370 
\subsection{Incorporating ML code}\label{sec:ML} 
7134  371 

8682  372 
\indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{MLcommand} 
373 
\indexisarcmd{MLsetup}\indexisarcmd{setup} 

9199  374 
\indexisarcmd{methodsetup} 
7134  375 
\begin{matharray}{rcl} 
376 
\isarcmd{use} & : & \isartrans{\cdot}{\cdot} \\ 

377 
\isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\ 

8682  378 
\isarcmd{ML_command} & : & \isartrans{\cdot}{\cdot} \\ 
7895  379 
\isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\ 
7175  380 
\isarcmd{setup} & : & \isartrans{theory}{theory} \\ 
9199  381 
\isarcmd{method_setup} & : & \isartrans{theory}{theory} \\ 
7134  382 
\end{matharray} 
383 

7895  384 
\railalias{MLsetup}{ML\_setup} 
385 
\railterm{MLsetup} 

386 

9199  387 
\railalias{methodsetup}{method\_setup} 
388 
\railterm{methodsetup} 

389 

8682  390 
\railalias{MLcommand}{ML\_command} 
391 
\railterm{MLcommand} 

392 

7134  393 
\begin{rail} 
9273  394 
'use' name comment? 
7134  395 
; 
9273  396 
('ML'  MLcommand  MLsetup  'setup') text comment? 
7134  397 
; 
9199  398 
methodsetup name '=' text text comment? 
399 
; 

7134  400 
\end{rail} 
401 

7167  402 
\begin{descr} 
7175  403 
\item [$\isarkeyword{use}~file$] reads and executes ML commands from $file$. 
7466  404 
The current theory context (if present) is passed down to the ML session, 
7981  405 
but may not be modified. Furthermore, the file name is checked with the 
7466  406 
$\isarkeyword{files}$ dependency declaration given in the theory header (see 
407 
also \S\ref{sec:beginthy}). 

408 

8682  409 
\item [$\isarkeyword{ML}~text$ and $\isarkeyword{ML_command}~text$] execute ML 
410 
commands from $text$. The theory context is passed in the same way as for 

411 
$\isarkeyword{use}$, but may not be changed. Note that 

412 
$\isarkeyword{ML_command}$ is less verbose than plain $\isarkeyword{ML}$. 

7895  413 

414 
\item [$\isarkeyword{ML_setup}~text$] executes ML commands from $text$. The 

415 
theory context is passed down to the ML session, and fetched back 

416 
afterwards. Thus $text$ may actually change the theory as a side effect. 

417 

7167  418 
\item [$\isarkeyword{setup}~text$] changes the current theory context by 
8379  419 
applying $text$, which refers to an ML expression of type 
420 
\texttt{(theory~>~theory)~list}. The $\isarkeyword{setup}$ command is the 

8547  421 
canonical way to initialize any objectlogic specific tools and packages 
422 
written in ML. 

9199  423 

424 
\item [$\isarkeyword{method_setup}~name = text~description$] defines a proof 

425 
method in the current theory. The given $text$ has to be an ML expression 

426 
of type \texttt{Args.src > Proof.context > Proof.method}. Parsing 

427 
concrete method syntax from \texttt{Args.src} input can be quite tedious in 

428 
general. The following simple examples are for methods without any explicit 

429 
arguments, or a list of theorems, respectively. 

430 

431 
{\footnotesize 

432 
\begin{verbatim} 

9605  433 
Method.no_args (Method.METHOD (fn facts => foobar_tac)) 
434 
Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac)) 

9199  435 
\end{verbatim} 
436 
} 

437 

438 
Note that mere tactic emulations may ignore the \texttt{facts} parameter 

439 
above. Proper proof methods would do something ``appropriate'' with the list 

440 
of current facts, though. Singlerule methods usually do strict 

441 
forwardchaining (e.g.\ by using \texttt{Method.multi_resolves}), while 

442 
automatic ones just insert the facts using \texttt{Method.insert_tac} before 

443 
applying the main tactic. 

7167  444 
\end{descr} 
7134  445 

446 

8250  447 
\subsection{Syntax translation functions} 
7134  448 

8250  449 
\indexisarcmd{parseasttranslation}\indexisarcmd{parsetranslation} 
450 
\indexisarcmd{printtranslation}\indexisarcmd{typedprinttranslation} 

451 
\indexisarcmd{printasttranslation}\indexisarcmd{tokentranslation} 

452 
\begin{matharray}{rcl} 

453 
\isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\ 

454 
\isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\ 

455 
\isarcmd{print_translation} & : & \isartrans{theory}{theory} \\ 

456 
\isarcmd{typed_print_translation} & : & \isartrans{theory}{theory} \\ 

457 
\isarcmd{print_ast_translation} & : & \isartrans{theory}{theory} \\ 

458 
\isarcmd{token_translation} & : & \isartrans{theory}{theory} \\ 

459 
\end{matharray} 

7134  460 

9273  461 
\railalias{parseasttranslation}{parse\_ast\_translation} 
462 
\railterm{parseasttranslation} 

463 

464 
\railalias{parsetranslation}{parse\_translation} 

465 
\railterm{parsetranslation} 

466 

467 
\railalias{printtranslation}{print\_translation} 

468 
\railterm{printtranslation} 

469 

470 
\railalias{typedprinttranslation}{typed\_print\_translation} 

471 
\railterm{typedprinttranslation} 

472 

473 
\railalias{printasttranslation}{print\_ast\_translation} 

474 
\railterm{printasttranslation} 

475 

476 
\railalias{tokentranslation}{token\_translation} 

477 
\railterm{tokentranslation} 

478 

479 
\begin{rail} 

480 
( parseasttranslation  parsetranslation  printtranslation  typedprinttranslation  

481 
printasttranslation  tokentranslation ) text comment? 

482 
\end{rail} 

483 

8250  484 
Syntax translation functions written in ML admit almost arbitrary 
485 
manipulations of Isabelle's inner syntax. Any of the above commands have a 

486 
single \railqtoken{text} argument that refers to an ML expression of 

8379  487 
appropriate type. 
488 

489 
\begin{ttbox} 

490 
val parse_ast_translation : (string * (ast list > ast)) list 

491 
val parse_translation : (string * (term list > term)) list 

492 
val print_translation : (string * (term list > term)) list 

493 
val typed_print_translation : 

494 
(string * (bool > typ > term list > term)) list 

495 
val print_ast_translation : (string * (ast list > ast)) list 

496 
val token_translation : 

497 
(string * string * (string > string * real)) list 

498 
\end{ttbox} 

499 
See \cite[\S8]{isabelleref} for more information on syntax transformations. 

7134  500 

501 

502 
\subsection{Oracles} 

503 

504 
\indexisarcmd{oracle} 

505 
\begin{matharray}{rcl} 

506 
\isarcmd{oracle} & : & \isartrans{theory}{theory} \\ 

507 
\end{matharray} 

508 

7175  509 
Oracles provide an interface to external reasoning systems, without giving up 
510 
control completely  each theorem carries a derivation object recording any 

511 
oracle invocation. See \cite[\S6]{isabelleref} for more information. 

512 

7134  513 
\begin{rail} 
514 
'oracle' name '=' text comment? 

515 
; 

516 
\end{rail} 

517 

7167  518 
\begin{descr} 
7175  519 
\item [$\isarkeyword{oracle}~name=text$] declares oracle $name$ to be ML 
8379  520 
function $text$, which has to be of type 
521 
\texttt{Sign.sg~*~Object.T~>~term}. 

7167  522 
\end{descr} 
7134  523 

524 

525 
\section{Proof commands} 

526 

7987  527 
Proof commands perform transitions of Isar/VM machine configurations, which 
7315  528 
are blockstructured, consisting of a stack of nodes with three main 
7335  529 
components: logical proof context, current facts, and open goals. Isar/VM 
8547  530 
transitions are \emph{typed} according to the following three different modes 
531 
of operation: 

7167  532 
\begin{descr} 
533 
\item [$proof(prove)$] means that a new goal has just been stated that is now 

8547  534 
to be \emph{proven}; the next command may refine it by some proof method, 
535 
and enter a subproof to establish the actual result. 

7167  536 
\item [$proof(state)$] is like an internal theory mode: the context may be 
7987  537 
augmented by \emph{stating} additional assumptions, intermediate results 
538 
etc. 

7895  539 
\item [$proof(chain)$] is intermediate between $proof(state)$ and 
7987  540 
$proof(prove)$: existing facts (i.e.\ the contents of the special ``$this$'' 
541 
register) have been just picked up in order to be used when refining the 

542 
goal claimed next. 

7167  543 
\end{descr} 
7134  544 

7167  545 

7895  546 
\subsection{Proof markup commands}\label{sec:markupprf} 
7167  547 

7987  548 
\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect} 
7895  549 
\indexisarcmd{txt}\indexisarcmd{txtraw} 
7134  550 
\begin{matharray}{rcl} 
8101  551 
\isarcmd{sect} & : & \isartrans{proof}{proof} \\ 
552 
\isarcmd{subsect} & : & \isartrans{proof}{proof} \\ 

553 
\isarcmd{subsubsect} & : & \isartrans{proof}{proof} \\ 

554 
\isarcmd{txt} & : & \isartrans{proof}{proof} \\ 

555 
\isarcmd{txt_raw} & : & \isartrans{proof}{proof} \\ 

7134  556 
\end{matharray} 
557 

7895  558 
These markup commands for proof mode closely correspond to the ones of theory 
8684  559 
mode (see \S\ref{sec:markupthy}). 
7895  560 

561 
\railalias{txtraw}{txt\_raw} 

562 
\railterm{txtraw} 

7175  563 

7134  564 
\begin{rail} 
7895  565 
('sect'  'subsect'  'subsubsect'  'txt'  txtraw) text 
7134  566 
; 
567 
\end{rail} 

568 

569 

7315  570 
\subsection{Proof context}\label{sec:proofcontext} 
7134  571 

7315  572 
\indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def} 
7134  573 
\begin{matharray}{rcl} 
574 
\isarcmd{fix} & : & \isartrans{proof(state)}{proof(state)} \\ 

575 
\isarcmd{assume} & : & \isartrans{proof(state)}{proof(state)} \\ 

576 
\isarcmd{presume} & : & \isartrans{proof(state)}{proof(state)} \\ 

577 
\isarcmd{def} & : & \isartrans{proof(state)}{proof(state)} \\ 

578 
\end{matharray} 

579 

7315  580 
The logical proof context consists of fixed variables and assumptions. The 
581 
former closely correspond to Skolem constants, or metalevel universal 

582 
quantification as provided by the Isabelle/Pure logical framework. 

583 
Introducing some \emph{arbitrary, but fixed} variable via $\FIX x$ results in 

7987  584 
a local value that may be used in the subsequent proof as any other variable 
7895  585 
or constant. Furthermore, any result $\edrv \phi[x]$ exported from the 
7987  586 
context will be universally closed wrt.\ $x$ at the outermost level: $\edrv 
587 
\All x \phi$ (this is expressed using Isabelle's metavariables). 

7315  588 

589 
Similarly, introducing some assumption $\chi$ has two effects. On the one 

590 
hand, a local theorem is created that may be used as a fact in subsequent 

7895  591 
proof steps. On the other hand, any result $\chi \drv \phi$ exported from the 
592 
context becomes conditional wrt.\ the assumption: $\edrv \chi \Imp \phi$. 

593 
Thus, solving an enclosing goal using such a result would basically introduce 

594 
a new subgoal stemming from the assumption. How this situation is handled 

595 
depends on the actual version of assumption command used: while $\ASSUMENAME$ 

596 
insists on solving the subgoal by unification with some premise of the goal, 

597 
$\PRESUMENAME$ leaves the subgoal unchanged in order to be proved later by the 

598 
user. 

7315  599 

7319  600 
Local definitions, introduced by $\DEF{}{x \equiv t}$, are achieved by 
7987  601 
combining $\FIX x$ with another version of assumption that causes any 
602 
hypothetical equation $x \equiv t$ to be eliminated by the reflexivity rule. 

603 
Thus, exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$. 

7175  604 

7134  605 
\begin{rail} 
7431  606 
'fix' (vars + 'and') comment? 
7134  607 
; 
7315  608 
('assume'  'presume') (assm comment? + 'and') 
7134  609 
; 
9471  610 
'def' thmdecl? \\ name '==' term termpat? comment? 
7134  611 
; 
612 

613 
var: name ('::' type)? 

614 
; 

7458  615 
vars: (name+) ('::' type)? 
7431  616 
; 
7315  617 
assm: thmdecl? (prop proppat? +) 
618 
; 

7134  619 
\end{rail} 
620 

7167  621 
\begin{descr} 
8547  622 
\item [$\FIX{\vec x}$] introduces local \emph{arbitrary, but fixed} variables 
623 
$\vec x$. 

8515  624 
\item [$\ASSUME{a}{\vec\phi}$ and $\PRESUME{a}{\vec\phi}$] introduce local 
625 
theorems $\vec\phi$ by assumption. Subsequent results applied to an 

626 
enclosing goal (e.g.\ by $\SHOWNAME$) are handled as follows: $\ASSUMENAME$ 

627 
expects to be able to unify with existing premises in the goal, while 

628 
$\PRESUMENAME$ leaves $\vec\phi$ as new subgoals. 

7335  629 

630 
Several lists of assumptions may be given (separated by 

7895  631 
$\isarkeyword{and}$); the resulting list of current facts consists of all of 
632 
these concatenated. 

7315  633 
\item [$\DEF{a}{x \equiv t}$] introduces a local (nonpolymorphic) definition. 
634 
In results exported from the context, $x$ is replaced by $t$. Basically, 

7987  635 
$\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\ASSUME{}{x \equiv t}$, with the 
7335  636 
resulting hypothetical equation solved by reflexivity. 
7431  637 

638 
The default name for the definitional equation is $x_def$. 

7167  639 
\end{descr} 
640 

7895  641 
The special name $prems$\indexisarthm{prems} refers to all assumptions of the 
642 
current context as a list of theorems. 

7315  643 

7167  644 

645 
\subsection{Facts and forward chaining} 

646 

647 
\indexisarcmd{note}\indexisarcmd{then}\indexisarcmd{from}\indexisarcmd{with} 

648 
\begin{matharray}{rcl} 

649 
\isarcmd{note} & : & \isartrans{proof(state)}{proof(state)} \\ 

650 
\isarcmd{then} & : & \isartrans{proof(state)}{proof(chain)} \\ 

651 
\isarcmd{from} & : & \isartrans{proof(state)}{proof(chain)} \\ 

652 
\isarcmd{with} & : & \isartrans{proof(state)}{proof(chain)} \\ 

653 
\end{matharray} 

654 

7319  655 
New facts are established either by assumption or proof of local statements. 
7335  656 
Any fact will usually be involved in further proofs, either as explicit 
8547  657 
arguments of proof methods, or when forward chaining towards the next goal via 
7335  658 
$\THEN$ (and variants). Note that the special theorem name 
7987  659 
$this$\indexisarthm{this} refers to the most recently established facts. 
7167  660 
\begin{rail} 
9199  661 
'note' (thmdef? thmrefs comment? + 'and') 
7167  662 
; 
663 
'then' comment? 

664 
; 

9199  665 
('from'  'with') (thmrefs comment? + 'and') 
7167  666 
; 
667 
\end{rail} 

668 

669 
\begin{descr} 

7175  670 
\item [$\NOTE{a}{\vec b}$] recalls existing facts $\vec b$, binding the result 
671 
as $a$. Note that attributes may be involved as well, both on the left and 

672 
right hand sides. 

7167  673 
\item [$\THEN$] indicates forward chaining by the current facts in order to 
7895  674 
establish the goal to be claimed next. The initial proof method invoked to 
675 
refine that will be offered the facts to do ``anything appropriate'' (cf.\ 

676 
also \S\ref{sec:proofsteps}). For example, method $rule$ (see 

8515  677 
\S\ref{sec:puremethatt}) would typically do an elimination rather than an 
7895  678 
introduction. Automatic methods usually insert the facts into the goal 
8547  679 
state before operation. This provides a simple scheme to control relevance 
680 
of facts in automated proof search. 

7335  681 
\item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; thus $\THEN$ is 
7458  682 
equivalent to $\FROM{this}$. 
7175  683 
\item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~facts}$; thus the forward 
684 
chaining is from earlier facts together with the current ones. 

7167  685 
\end{descr} 
686 

8515  687 
Basic proof methods (such as $rule$, see \S\ref{sec:puremethatt}) expect 
7895  688 
multiple facts to be given in their proper order, corresponding to a prefix of 
689 
the premises of the rule involved. Note that positions may be easily skipped 

9695  690 
using something like $\FROM{\Text{\texttt{_}}~a~b}$, for example. This 
8547  691 
involves the trivial rule $\PROP\psi \Imp \PROP\psi$, which happens to be 
692 
bound in Isabelle/Pure as ``\texttt{_}'' 

693 
(underscore).\indexisarthm{_@\texttt{_}} 

7389  694 

9238  695 
Forward chaining with an empty list of theorems is the same as not chaining. 
696 
Thus $\FROM{nothing}$ has no effect apart from entering $prove(chain)$ mode, 

697 
since $nothing$\indexisarthm{nothing} is bound to the empty list of facts. 

698 

7167  699 

700 
\subsection{Goal statements} 

701 

702 
\indexisarcmd{theorem}\indexisarcmd{lemma} 

703 
\indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus} 

704 
\begin{matharray}{rcl} 

705 
\isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\ 

706 
\isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\ 

7987  707 
\isarcmd{have} & : & \isartrans{proof(state) ~~ proof(chain)}{proof(prove)} \\ 
708 
\isarcmd{show} & : & \isartrans{proof(state) ~~ proof(chain)}{proof(prove)} \\ 

7167  709 
\isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\ 
710 
\isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\ 

711 
\end{matharray} 

712 

7175  713 
Proof mode is entered from theory mode by initial goal commands $\THEOREMNAME$ 
7895  714 
and $\LEMMANAME$. New local goals may be claimed within proof mode as well. 
715 
Four variants are available, indicating whether the result is meant to solve 

8547  716 
some pending goal or whether forward chaining is indicated. 
7175  717 

7167  718 
\begin{rail} 
719 
('theorem'  'lemma') goal 

720 
; 

721 
('have'  'show'  'hence'  'thus') goal 

722 
; 

723 

8632  724 
goal: thmdecl? prop proppat? comment? 
7167  725 
; 
726 
\end{rail} 

727 

728 
\begin{descr} 

7335  729 
\item [$\THEOREM{a}{\phi}$] enters proof mode with $\phi$ as main goal, 
8547  730 
eventually resulting in some theorem $\turn \phi$ to be put back into the 
731 
theory. 

7987  732 
\item [$\LEMMA{a}{\phi}$] is similar to $\THEOREMNAME$, but tags the result as 
7167  733 
``lemma''. 
7335  734 
\item [$\HAVE{a}{\phi}$] claims a local goal, eventually resulting in a 
7167  735 
theorem with the current assumption context as hypotheses. 
7335  736 
\item [$\SHOW{a}{\phi}$] is similar to $\HAVE{a}{\phi}$, but solves some 
7895  737 
pending goal with the result \emph{exported} into the corresponding context 
738 
(cf.\ \S\ref{sec:proofcontext}). 

739 
\item [$\HENCENAME$] abbreviates $\THEN~\HAVENAME$, i.e.\ claims a local goal 

740 
to be proven by forward chaining the current facts. Note that $\HENCENAME$ 

741 
is also equivalent to $\FROM{this}~\HAVENAME$. 

742 
\item [$\THUSNAME$] abbreviates $\THEN~\SHOWNAME$. Note that $\THUSNAME$ is 

743 
also equivalent to $\FROM{this}~\SHOWNAME$. 

7167  744 
\end{descr} 
745 

8991  746 
Note that any goal statement causes some term abbreviations (such as 
747 
$\Var{thesis}$, $\dots$) to be bound automatically, see also 

748 
\S\ref{sec:termabbrev}. Furthermore, the local context of a (nonatomic) 

749 
goal is provided via the case name $antecedent$\indexisarcase{antecedent}, see 

750 
also \S\ref{sec:cases}. 

751 

7167  752 

753 
\subsection{Initial and terminal proof steps}\label{sec:proofsteps} 

754 

7175  755 
\indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by} 
756 
\indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry} 

757 
\begin{matharray}{rcl} 

758 
\isarcmd{proof} & : & \isartrans{proof(prove)}{proof(state)} \\ 

759 
\isarcmd{qed} & : & \isartrans{proof(state)}{proof(state) ~~ theory} \\ 

760 
\isarcmd{by} & : & \isartrans{proof(prove)}{proof(state) ~~ theory} \\ 

761 
\isarcmd{.\,.} & : & \isartrans{proof(prove)}{proof(state) ~~ theory} \\ 

762 
\isarcmd{.} & : & \isartrans{proof(prove)}{proof(state) ~~ theory} \\ 

763 
\isarcmd{sorry} & : & \isartrans{proof(prove)}{proof(state) ~~ theory} \\ 

764 
\end{matharray} 

765 

8547  766 
Arbitrary goal refinement via tactics is considered harmful. Properly, the 
7335  767 
Isar framework admits proof methods to be invoked in two places only. 
7167  768 
\begin{enumerate} 
7175  769 
\item An \emph{initial} refinement step $\PROOF{m@1}$ reduces a newly stated 
7335  770 
goal to a number of subgoals that are to be solved later. Facts are passed 
7895  771 
to $m@1$ for forward chaining, if so indicated by $proof(chain)$ mode. 
7167  772 

7987  773 
\item A \emph{terminal} conclusion step $\QED{m@2}$ is intended to solve 
774 
remaining goals. No facts are passed to $m@2$. 

7167  775 
\end{enumerate} 
776 

8547  777 
The only other proper way to affect pending goals is by $\SHOWNAME$, which 
778 
involves an explicit statement of what is to be solved. 

7167  779 

7175  780 
\medskip 
781 

7167  782 
Also note that initial proof methods should either solve the goal completely, 
7895  783 
or constitute some wellunderstood reduction to new subgoals. Arbitrary 
784 
automatic proof tools that are prone leave a large number of badly structured 

785 
subgoals are no help in continuing the proof document in any intelligible 

7987  786 
way. 
7167  787 

7175  788 
\medskip 
789 

8547  790 
Unless given explicitly by the user, the default initial method is ``$rule$'', 
791 
which applies a single standard elimination or introduction rule according to 

792 
the topmost symbol involved. There is no separate default terminal method. 

793 
Any remaining goals are always solved by assumption in the very last step. 

7167  794 

795 
\begin{rail} 

796 
'proof' interest? meth? comment? 

797 
; 

798 
'qed' meth? comment? 

799 
; 

800 
'by' meth meth? comment? 

801 
; 

802 
('.'  '..'  'sorry') comment? 

803 
; 

804 

805 
meth: method interest? 

806 
; 

807 
\end{rail} 

808 

809 
\begin{descr} 

7335  810 
\item [$\PROOF{m@1}$] refines the goal by proof method $m@1$; facts for 
811 
forward chaining are passed if so indicated by $proof(chain)$ mode. 

812 
\item [$\QED{m@2}$] refines any remaining goals by proof method $m@2$ and 

7895  813 
concludes the subproof by assumption. If the goal had been $\SHOWNAME$ (or 
814 
$\THUSNAME$), some pending subgoal is solved as well by the rule resulting 

815 
from the result \emph{exported} into the enclosing goal context. Thus 

816 
$\QEDNAME$ may fail for two reasons: either $m@2$ fails, or the resulting 

817 
rule does not fit to any pending goal\footnote{This includes any additional 

818 
``strong'' assumptions as introduced by $\ASSUMENAME$.} of the enclosing 

819 
context. Debugging such a situation might involve temporarily changing 

820 
$\SHOWNAME$ into $\HAVENAME$, or weakening the local context by replacing 

821 
some occurrences of $\ASSUMENAME$ by $\PRESUMENAME$. 

822 
\item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}\index{proof!terminal}; it 

7987  823 
abbreviates $\PROOF{m@1}~\QED{m@2}$, with backtracking across both methods, 
824 
though. Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done 

7895  825 
by expanding its definition; in many cases $\PROOF{m@1}$ is already 
7175  826 
sufficient to see what is going wrong. 
7895  827 
\item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it 
8515  828 
abbreviates $\BY{rule}$. 
7895  829 
\item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it 
8195  830 
abbreviates $\BY{this}$. 
8379  831 
\item [$\SORRY$] is a \emph{fake proof}\index{proof!fake}; provided that the 
832 
\texttt{quick_and_dirty} flag is enabled, $\SORRY$ pretends to solve the 

8515  833 
goal without further ado. Of course, the result would be a fake theorem 
834 
only, involving some oracle in its internal derivation object (this is 

835 
indicated as ``$[!]$'' in the printed result). The main application of 

836 
$\SORRY$ is to support experimentation and topdown proof development. 

837 
\end{descr} 

838 

839 

840 
\subsection{Fundamental methods and attributes}\label{sec:puremethatt} 

841 

8547  842 
The following proof methods and attributes refer to basic logical operations 
843 
of Isar. Further methods and attributes are provided by several generic and 

844 
objectlogic specific tools and packages (see chapters \ref{ch:gentools} and 

845 
\ref{ch:holtools}). 

8515  846 

847 
\indexisarmeth{assumption}\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{$$} 

9936  848 
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}\indexisaratt{rule} 
8515  849 
\indexisaratt{OF}\indexisaratt{of} 
850 
\begin{matharray}{rcl} 

851 
assumption & : & \isarmeth \\ 

852 
this & : & \isarmeth \\ 

853 
rule & : & \isarmeth \\ 

854 
 & : & \isarmeth \\ 

855 
OF & : & \isaratt \\ 

856 
of & : & \isaratt \\ 

857 
intro & : & \isaratt \\ 

858 
elim & : & \isaratt \\ 

859 
dest & : & \isaratt \\ 

9936  860 
rule & : & \isaratt \\ 
8515  861 
\end{matharray} 
862 

863 
\begin{rail} 

8547  864 
'rule' thmrefs? 
8515  865 
; 
866 
'OF' thmrefs 

867 
; 

8693  868 
'of' insts ('concl' ':' insts)? 
8515  869 
; 
9936  870 
'rule' 'del' 
871 
; 

8515  872 
\end{rail} 
873 

874 
\begin{descr} 

875 
\item [$assumption$] solves some goal by a single assumption step. Any facts 

876 
given (${} \le 1$) are guaranteed to participate in the refinement. Recall 

877 
that $\QEDNAME$ (see \S\ref{sec:proofsteps}) already concludes any 

878 
remaining subgoals by assumption. 

879 
\item [$this$] applies all of the current facts directly as rules. Recall 

880 
that ``$\DOT$'' (dot) abbreviates $\BY{this}$. 

8547  881 
\item [$rule~\vec a$] applies some rule given as argument in backward manner; 
8515  882 
facts are used to reduce the rule before applying it to the goal. Thus 
883 
$rule$ without facts is plain \emph{introduction}, while with facts it 

884 
becomes \emph{elimination}. 

885 

8547  886 
When no arguments are given, the $rule$ method tries to pick appropriate 
887 
rules automatically, as declared in the current context using the $intro$, 

888 
$elim$, $dest$ attributes (see below). This is the default behavior of 

889 
$\PROOFNAME$ and ``$\DDOT$'' (doubledot) steps (see 

8515  890 
\S\ref{sec:proofsteps}). 
891 
\item [``$$''] does nothing but insert the forward chaining facts as premises 

892 
into the goal. Note that command $\PROOFNAME$ without any method actually 

893 
performs a single reduction step using the $rule$ method; thus a plain 

894 
\emph{donothing} proof step would be $\PROOF{}$ rather than $\PROOFNAME$ 

895 
alone. 

8547  896 
\item [$OF~\vec a$] applies some theorem to given rules $\vec a$ (in 
897 
parallel). This corresponds to the \texttt{MRS} operator in ML 

898 
\cite[\S5]{isabelleref}, but note the reversed order. Positions may be 

899 
skipped by including ``$\_$'' (underscore) as argument. 

900 
\item [$of~\vec t$] performs positional instantiation. The terms $\vec t$ are 

8515  901 
substituted for any schematic variables occurring in a theorem from left to 
902 
right; ``\texttt{_}'' (underscore) indicates to skip a position. Arguments 

903 
following a ``$concl\colon$'' specification refer to positions of the 

904 
conclusion of a rule. 

905 
\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and 

906 
destruct rules, respectively. Note that the classical reasoner (see 

907 
\S\ref{sec:classicalbasic}) introduces different versions of these 

908 
attributes, and the $rule$ method, too. In objectlogics with classical 

909 
reasoning enabled, the latter version should be used all the time to avoid 

910 
confusion! 

9936  911 
\item [$rule~del$] undeclares introduction, elimination, or destruct rules. 
7315  912 
\end{descr} 
913 

914 

915 
\subsection{Term abbreviations}\label{sec:termabbrev} 

916 

917 
\indexisarcmd{let} 

918 
\begin{matharray}{rcl} 

919 
\isarcmd{let} & : & \isartrans{proof(state)}{proof(state)} \\ 

920 
\isarkeyword{is} & : & syntax \\ 

921 
\end{matharray} 

922 

923 
Abbreviations may be either bound by explicit $\LET{p \equiv t}$ statements, 

7987  924 
or by annotating assumptions or goal statements with a list of patterns 
925 
$\ISS{p@1\;\dots}{p@n}$. In both cases, higherorder matching is invoked to 

926 
bind extralogical term variables, which may be either named schematic 

927 
variables of the form $\Var{x}$, or nameless dummies ``\texttt{_}'' 

928 
(underscore).\indexisarvar{_@\texttt{_}} Note that in the $\LETNAME$ form the 

929 
patterns occur on the lefthand side, while the $\ISNAME$ patterns are in 

930 
postfix position. 

7315  931 

8620
3786d47f5570
support HindleyMilner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset

932 
Polymorphism of term bindings is handled in HindleyMilner style, as in ML. 
3786d47f5570
support HindleyMilner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset

933 
Type variables referring to local assumptions or open goal statements are 
3786d47f5570
support HindleyMilner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset

934 
\emph{fixed}, while those of finished results or bound by $\LETNAME$ may occur 
3786d47f5570
support HindleyMilner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset

935 
in \emph{arbitrary} instances later. Even though actual polymorphism should 
3786d47f5570
support HindleyMilner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset

936 
be rarely used in practice, this mechanism is essential to achieve proper 
3786d47f5570
support HindleyMilner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset

937 
incremental typeinference, as the user proceeds to build up the Isar proof 
3786d47f5570
support HindleyMilner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset

938 
text. 
3786d47f5570
support HindleyMilner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset

939 

3786d47f5570
support HindleyMilner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset

940 
\medskip 
3786d47f5570
support HindleyMilner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset

941 

7319  942 
Term abbreviations are quite different from actual local definitions as 
943 
introduced via $\DEFNAME$ (see \S\ref{sec:proofcontext}). The latter are 

7315  944 
visible within the logic as actual equations, while abbreviations disappear 
8620
3786d47f5570
support HindleyMilner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset

945 
during the input process just after type checking. Also note that $\DEFNAME$ 
3786d47f5570
support HindleyMilner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset

946 
does not support polymorphism. 
7315  947 

948 
\begin{rail} 

8664  949 
'let' ((term + 'and') '=' term comment? + 'and') 
7315  950 
; 
951 
\end{rail} 

952 

953 
The syntax of $\ISNAME$ patterns follows \railnonterm{termpat} or 

954 
\railnonterm{proppat} (see \S\ref{sec:termpats}). 

955 

956 
\begin{descr} 

957 
\item [$\LET{\vec p = \vec t}$] binds any text variables in patters $\vec p$ 

958 
by simultaneous higherorder matching against terms $\vec t$. 

959 
\item [$\IS{\vec p}$] resembles $\LETNAME$, but matches $\vec p$ against the 

960 
preceding statement. Also note that $\ISNAME$ is not a separate command, 

961 
but part of others (such as $\ASSUMENAME$, $\HAVENAME$ etc.). 

962 
\end{descr} 

963 

10160  964 
Some \emph{automatic} term abbreviations\index{term abbreviations} for goals 
7988  965 
and facts are available as well. For any open goal, 
10160  966 
$\Var{thesis}$\indexisarvar{thesis} refers to its objectlevel statement, 
967 
abstracted over any metalevel parameters (if present). Likewise, 

968 
$\Var{this}$\indexisarvar{this} is bound for fact statements resulting from 

969 
assumptions or finished goals. In case $\Var{this}$ refers to an objectlogic 

970 
statement that is an application $f(t)$, then $t$ is bound to the special text 

971 
variable ``$\dots$''\indexisarvar{\dots} (three dots). The canonical 

972 
application of the latter are calculational proofs (see 

973 
\S\ref{sec:calculation}). 

974 

975 
%FIXME !? 

7315  976 

10160  977 
% A few \emph{automatic} term abbreviations\index{term abbreviations} for goals 
978 
% and facts are available as well. For any open goal, 

979 
% $\Var{thesis_prop}$\indexisarvar{thesisprop} refers to the full proposition 

980 
% (which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesisconcl} to its 

981 
% (atomic) conclusion, and $\Var{thesis}$\indexisarvar{thesis} to its 

982 
% objectlevel statement. The latter two abstract over any metalevel 

983 
% parameters. 

984 

985 
% Fact statements resulting from assumptions or finished goals are bound as 

986 
% $\Var{this_prop}$\indexisarvar{thisprop}, 

987 
% $\Var{this_concl}$\indexisarvar{thisconcl}, and 

988 
% $\Var{this}$\indexisarvar{this}, similar to $\Var{thesis}$ above. In case 

989 
% $\Var{this}$ refers to an objectlogic statement that is an application 

990 
% $f(t)$, then $t$ is bound to the special text variable 

991 
% ``$\dots$''\indexisarvar{\dots} (three dots). The canonical application of 

992 
% the latter are calculational proofs (see \S\ref{sec:calculation}). 

7315  993 

994 

7134  995 
\subsection{Block structure} 
996 

8896  997 
\indexisarcmd{next}\indexisarcmd{\{}\indexisarcmd{\}} 
7397  998 
\begin{matharray}{rcl} 
8448  999 
\NEXT & : & \isartrans{proof(state)}{proof(state)} \\ 
7974  1000 
\BG & : & \isartrans{proof(state)}{proof(state)} \\ 
1001 
\EN & : & \isartrans{proof(state)}{proof(state)} \\ 

7397  1002 
\end{matharray} 
1003 

9030  1004 
\railalias{lbrace}{\ttlbrace} 
1005 
\railterm{lbrace} 

1006 

1007 
\railalias{rbrace}{\ttrbrace} 

1008 
\railterm{rbrace} 

1009 

1010 
\begin{rail} 

1011 
'next' comment? 

1012 
; 

1013 
lbrace comment? 

1014 
; 

1015 
rbrace comment? 

1016 
; 

1017 
\end{rail} 

1018 

7167  1019 
While Isar is inherently blockstructured, opening and closing blocks is 
1020 
mostly handled rather casually, with little explicit userintervention. Any 

1021 
local goal statement automatically opens \emph{two} blocks, which are closed 

1022 
again when concluding the subproof (by $\QEDNAME$ etc.). Sections of 

8448  1023 
different context within a subproof may be switched via $\NEXT$, which is 
1024 
just a single blockclose followed by blockopen again. Thus the effect of 

1025 
$\NEXT$ to reset the local proof context. There is no goal focus involved 

1026 
here! 

7167  1027 

7175  1028 
For slightly more advanced applications, there are explicit block parentheses 
7895  1029 
as well. These typically achieve a stronger forward style of reasoning. 
7167  1030 

1031 
\begin{descr} 

8448  1032 
\item [$\NEXT$] switches to a fresh block within a subproof, resetting the 
1033 
local context to the initial one. 

8896  1034 
\item [$\BG$ and $\EN$] explicitly open and close blocks. Any current facts 
1035 
pass through ``$\BG$'' unchanged, while ``$\EN$'' causes any result to be 

7895  1036 
\emph{exported} into the enclosing context. Thus fixed variables are 
1037 
generalized, assumptions discharged, and local definitions unfolded (cf.\ 

1038 
\S\ref{sec:proofcontext}). There is no difference of $\ASSUMENAME$ and 

1039 
$\PRESUMENAME$ in this mode of forward reasoning  in contrast to plain 

1040 
backward reasoning with the result exported at $\SHOWNAME$ time. 

7167  1041 
\end{descr} 
7134  1042 

1043 

9605  1044 
\subsection{Emulating tactic scripts}\label{sec:tacticcommands} 
8515  1045 

9605  1046 
The Isar provides separate commands to accommodate tacticstyle proof scripts 
1047 
within the same system. While being outside the orthodox Isar proof language, 

1048 
these might come in handy for interactive exploration and debugging, or even 

1049 
actual tactical proof within newstyle theories (to benefit from document 

1050 
preparation, for example). See also \S\ref{sec:tactics} for actual tactics, 

1051 
that have been encapsulated as proof methods. Proper proof methods may be 

1052 
used in scripts, too. 

8515  1053 

9605  1054 
\indexisarcmd{apply}\indexisarcmd{applyend}\indexisarcmd{done} 
8515  1055 
\indexisarcmd{defer}\indexisarcmd{prefer}\indexisarcmd{back} 
9605  1056 
\indexisarcmd{declare} 
8515  1057 
\begin{matharray}{rcl} 
8533  1058 
\isarcmd{apply}^* & : & \isartrans{proof(prove)}{proof(prove)} \\ 
9605  1059 
\isarcmd{apply_end}^* & : & \isartrans{proof(state)}{proof(state)} \\ 
8946  1060 
\isarcmd{done}^* & : & \isartrans{proof(prove)}{proof(state)} \\ 
8533  1061 
\isarcmd{defer}^* & : & \isartrans{proof}{proof} \\ 
1062 
\isarcmd{prefer}^* & : & \isartrans{proof}{proof} \\ 

1063 
\isarcmd{back}^* & : & \isartrans{proof}{proof} \\ 

9605  1064 
\isarcmd{declare}^* & : & \isartrans{theory}{theory} \\ 
8515  1065 
\end{matharray} 
1066 

1067 
\railalias{applyend}{apply\_end} 

1068 
\railterm{applyend} 

1069 

1070 
\begin{rail} 

9605  1071 
( 'apply'  applyend ) method comment? 
8515  1072 
; 
8946  1073 
'done' comment? 
1074 
; 

8682  1075 
'defer' nat? comment? 
8515  1076 
; 
8682  1077 
'prefer' nat comment? 
8515  1078 
; 
9273  1079 
'back' comment? 
1080 
; 

9605  1081 
'declare' thmrefs comment? 
1082 
; 

8515  1083 
\end{rail} 
1084 

1085 
\begin{descr} 

10223  1086 
\item [$\APPLY{m}$] applies proof method $m$ in initial position, but unlike 
1087 
$\PROOFNAME$ it retains ``$proof(prove)$'' mode. Thus consecutive method 

1088 
applications may be given just as in tactic scripts. 

8515  1089 

8881  1090 
Facts are passed to $m$ as indicated by the goal's forwardchain mode, and 
10223  1091 
are \emph{consumed} afterwards. Thus any further $\APPLYNAME$ command would 
1092 
always work in a purely backward manner. 

8946  1093 

8515  1094 
\item [$\isarkeyword{apply_end}~(m)$] applies proof method $m$ as if in 
1095 
terminal position. Basically, this simulates a multistep tactic script for 

1096 
$\QEDNAME$, but may be given anywhere within the proof body. 

1097 

1098 
No facts are passed to $m$. Furthermore, the static context is that of the 

1099 
enclosing goal (as for actual $\QEDNAME$). Thus the proof method may not 

1100 
refer to any assumptions introduced in the current body, for example. 

9605  1101 

1102 
\item [$\isarkeyword{done}$] completes a proof script, provided that the 

1103 
current goal state is already solved completely. Note that actual 

1104 
structured proof commands (e.g.\ ``$\DOT$'' or $\SORRY$) may be used to 

1105 
conclude proof scripts as well. 

1106 

8515  1107 
\item [$\isarkeyword{defer}~n$ and $\isarkeyword{prefer}~n$] shuffle the list 
1108 
of pending goals: $defer$ puts off goal $n$ to the end of the list ($n = 1$ 

1109 
by default), while $prefer$ brings goal $n$ to the top. 

9605  1110 

8515  1111 
\item [$\isarkeyword{back}$] does backtracking over the result sequence of 
1112 
the latest proof command.\footnote{Unlike the ML function \texttt{back} 

1113 
\cite{isabelleref}, the Isar command does not search upwards for further 

1114 
branch points.} Basically, any proof command may return multiple results. 

9605  1115 

1116 
\item [$\isarkeyword{declare}~thms$] declares theorems to the current theory 

1117 
context. No theorem binding is involved here, unlike 

1118 
$\isarkeyword{theorems}$ or $\isarkeyword{lemmas}$ (cf.\ 

1119 
\S\ref{sec:axmsthms}). So $\isarkeyword{declare}$ only has the effect of 

1120 
applying attributes as included in the theorem specification. 

9006  1121 
\end{descr} 
1122 

1123 
Any proper Isar proof method may be used with tactic script commands such as 

10223  1124 
$\APPLYNAME$. A few additional emulations of actual tactics are provided as 
1125 
well; these would be never used in actual structured proofs, of course. 

9006  1126 

8515  1127 

1128 
\subsection{Metalinguistic features} 

1129 

1130 
\indexisarcmd{oops} 

1131 
\begin{matharray}{rcl} 

1132 
\isarcmd{oops} & : & \isartrans{proof}{theory} \\ 

1133 
\end{matharray} 

1134 

1135 
The $\OOPS$ command discontinues the current proof attempt, while considering 

1136 
the partial proof text as properly processed. This is conceptually quite 

1137 
different from ``faking'' actual proofs via $\SORRY$ (see 

1138 
\S\ref{sec:proofsteps}): $\OOPS$ does not observe the proof structure at all, 

1139 
but goes back right to the theory level. Furthermore, $\OOPS$ does not 

1140 
produce any result theorem  there is no claim to be able to complete the 

1141 
proof anyhow. 

1142 

1143 
A typical application of $\OOPS$ is to explain Isar proofs \emph{within} the 

1144 
system itself, in conjunction with the document preparation tools of Isabelle 

1145 
described in \cite{isabellesys}. Thus partial or even wrong proof attempts 

1146 
can be discussed in a logically sound manner. Note that the Isabelle {\LaTeX} 

1147 
macros can be easily adapted to print something like ``$\dots$'' instead of an 

1148 
``$\OOPS$'' keyword. 

1149 

8547  1150 
\medskip The $\OOPS$ command is undoable, unlike $\isarkeyword{kill}$ (see 
1151 
\S\ref{sec:history}). The effect is to get back to the theory \emph{before} 

1152 
the opening of the proof. 

8515  1153 

1154 

7134  1155 
\section{Other commands} 
1156 

9605  1157 
\subsection{Diagnostics} 
7134  1158 

8485  1159 
\indexisarcmd{pr}\indexisarcmd{thm}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{typ} 
7134  1160 
\begin{matharray}{rcl} 
8515  1161 
\isarcmd{pr}^* & : & \isarkeep{\cdot} \\ 
1162 
\isarcmd{thm}^* & : & \isarkeep{theory~~proof} \\ 

1163 
\isarcmd{term}^* & : & \isarkeep{theory~~proof} \\ 

1164 
\isarcmd{prop}^* & : & \isarkeep{theory~~proof} \\ 

1165 
\isarcmd{typ}^* & : & \isarkeep{theory~~proof} \\ 

7134  1166 
\end{matharray} 
1167 

9605  1168 
These diagnostic commands assist interactive development. Note that $undo$ 
1169 
does not apply here, the theory or proof configuration is not changed. 

7335  1170 

7134  1171 
\begin{rail} 
9727  1172 
'pr' modes? nat? (',' nat)? 
7134  1173 
; 
8485  1174 
'thm' modes? thmrefs 
1175 
; 

1176 
'term' modes? term 

7134  1177 
; 
8485  1178 
'prop' modes? prop 
7134  1179 
; 
8485  1180 
'typ' modes? type 
1181 
; 

1182 

1183 
modes: '(' (name + ) ')' 

7134  1184 
; 
1185 
\end{rail} 

1186 

7167  1187 
\begin{descr} 
9727  1188 
\item [$\isarkeyword{pr}~goals, prems$] prints the current proof state (if 
1189 
present), including the proof context, current facts and goals. The 

1190 
optional limit arguments affect the number of goals and premises to be 

1191 
displayed, which is initially 10 for both. Omitting limit values leaves the 

1192 
current setting unchanged. 

8547  1193 
\item [$\isarkeyword{thm}~\vec a$] retrieves theorems from the current theory 
1194 
or proof context. Note that any attributes included in the theorem 

7974  1195 
specifications are applied to a temporary context derived from the current 
8547  1196 
theory or proof; the result is discarded, i.e.\ attributes involved in $\vec 
1197 
a$ do not have any permanent effect. 

9727  1198 
\item [$\isarkeyword{term}~t$ and $\isarkeyword{prop}~\phi$] read, typecheck 
1199 
and print terms or propositions according to the current theory or proof 

7895  1200 
context; the inferred type of $t$ is output as well. Note that these 
1201 
commands are also useful in inspecting the current environment of term 

1202 
abbreviations. 

7974  1203 
\item [$\isarkeyword{typ}~\tau$] reads and prints types of the metalogic 
1204 
according to the current theory or proof context. 

9605  1205 
\end{descr} 
1206 

1207 
All of the diagnostic commands above admit a list of $modes$ to be specified, 

1208 
which is appended to the current print mode (see also \cite{isabelleref}). 

1209 
Thus the output behavior may be modified according particular print mode 

1210 
features. For example, $\isarkeyword{pr}~(latex~xsymbols~symbols)$ would 

1211 
print the current proof state with mathematical symbols and special characters 

1212 
represented in {\LaTeX} source, according to the Isabelle style 

1213 
\cite{isabellesys}. 

1214 

1215 
Note that antiquotations (cf.\ \S\ref{sec:antiq}) provide a more systematic 

1216 
way to include formal items into the printed text document. 

1217 

1218 

1219 
\subsection{Inspecting the context} 

1220 

1221 
\indexisarcmd{printfacts}\indexisarcmd{printbinds} 

1222 
\indexisarcmd{printcommands}\indexisarcmd{printsyntax} 

1223 
\indexisarcmd{printmethods}\indexisarcmd{printattributes} 

1224 
\begin{matharray}{rcl} 

1225 
\isarcmd{print_commands}^* & : & \isarkeep{\cdot} \\ 

1226 
\isarcmd{print_syntax}^* & : & \isarkeep{theory~~proof} \\ 

1227 
\isarcmd{print_methods}^* & : & \isarkeep{theory~~proof} \\ 

1228 
\isarcmd{print_attributes}^* & : & \isarkeep{theory~~proof} \\ 

1229 
\isarcmd{print_facts}^* & : & \isarkeep{proof} \\ 

1230 
\isarcmd{print_binds}^* & : & \isarkeep{proof} \\ 

1231 
\end{matharray} 

1232 

1233 
These commands print parts of the theory and proof context. Note that there 

1234 
are some further ones available, such as for the set of rules declared for 

1235 
simplifications. 

1236 

1237 
\begin{descr} 

1238 
\item [$\isarkeyword{print_commands}$] prints Isabelle's outer theory syntax, 

1239 
including keywords and command. 

1240 
\item [$\isarkeyword{print_syntax}$] prints the inner syntax of types and 

1241 
terms, depending on the current context. The output can be very verbose, 

1242 
including grammar tables and syntax translation rules. See \cite[\S7, 

1243 
\S8]{isabelleref} for further information on Isabelle's inner syntax. 

1244 
\item [$\isarkeyword{print_methods}$] all proof methods available in the 

1245 
current theory context. 

1246 
\item [$\isarkeyword{print_attributes}$] all attributes available in the 

1247 
current theory context. 

8379  1248 
\item [$\isarkeyword{print_facts}$] prints any named facts of the current 
1249 
context, including assumptions and local results. 

1250 
\item [$\isarkeyword{print_binds}$] prints all term abbreviations present in 

1251 
the context. 

8485  1252 
\end{descr} 
1253 

1254 

1255 
\subsection{History commands}\label{sec:history} 

1256 

1257 
\indexisarcmd{undo}\indexisarcmd{redo}\indexisarcmd{kill} 

1258 
\begin{matharray}{rcl} 

1259 
\isarcmd{undo}^{{*}{*}} & : & \isarkeep{\cdot} \\ 

1260 
\isarcmd{redo}^{{*}{*}} & : & \isarkeep{\cdot} \\ 

1261 
\isarcmd{kill}^{{*}{*}} & : & \isarkeep{\cdot} \\ 

1262 
\end{matharray} 

1263 

1264 
The Isabelle/Isar toplevel maintains a twostage history, for theory and 

1265 
proof state transformation. Basically, any command can be undone using 

1266 
$\isarkeyword{undo}$, excluding mere diagnostic elements. Its effect may be 

1267 
revoked via $\isarkeyword{redo}$, unless the corresponding the 

1268 
$\isarkeyword{undo}$ step has crossed the beginning of a proof or theory. The 

1269 
$\isarkeyword{kill}$ command aborts the current history node altogether, 

1270 
discontinuing a proof or even the whole theory. This operation is \emph{not} 

1271 
undoable. 

1272 

1273 
\begin{warn} 

8547  1274 
History commands should never be used with user interfaces such as 
1275 
Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes care of 

1276 
stepping forth and back itself. Interfering by manual $\isarkeyword{undo}$, 

8510  1277 
$\isarkeyword{redo}$, or even $\isarkeyword{kill}$ commands would quickly 
1278 
result in utter confusion. 

8485  1279 
\end{warn} 
1280 

8379  1281 

7134  1282 
\subsection{System operations} 
1283 

7167  1284 
\indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{usethy}\indexisarcmd{usethyonly} 
1285 
\indexisarcmd{updatethy}\indexisarcmd{updatethyonly} 

7134  1286 
\begin{matharray}{rcl} 
8515  1287 
\isarcmd{cd}^* & : & \isarkeep{\cdot} \\ 
1288 
\isarcmd{pwd}^* & : & \isarkeep{\cdot} \\ 

1289 
\isarcmd{use_thy}^* & : & \isarkeep{\cdot} \\ 

1290 
\isarcmd{use_thy_only}^* & : & \isarkeep{\cdot} \\ 

1291 
\isarcmd{update_thy}^* & : & \isarkeep{\cdot} \\ 

1292 
\isarcmd{update_thy_only}^* & : & \isarkeep{\cdot} \\ 

7134  1293 
\end{matharray} 
1294 

7167  1295 
\begin{descr} 
7134  1296 
\item [$\isarkeyword{cd}~name$] changes the current directory of the Isabelle 
1297 
process. 

1298 
\item [$\isarkeyword{pwd}~$] prints the current working directory. 

7175  1299 
\item [$\isarkeyword{use_thy}$, $\isarkeyword{use_thy_only}$, 
7987  1300 
$\isarkeyword{update_thy}$, $\isarkeyword{update_thy_only}$] load some 
7895  1301 
theory given as $name$ argument. These commands are basically the same as 
7987  1302 
the corresponding ML functions\footnote{The ML versions also change the 
1303 
implicit theory context to that of the theory loaded.} (see also 

1304 
\cite[\S1,\S6]{isabelleref}). Note that both the ML and Isar versions may 

1305 
load new and oldstyle theories alike. 

7167  1306 
\end{descr} 
7134  1307 

7987  1308 
These system commands are scarcely used when working with the Proof~General 
1309 
interface, since loading of theories is done fully transparently. 

7134  1310 

8379  1311 

7046  1312 
%%% Local Variables: 
1313 
%%% mode: latex 

1314 
%%% TeXmaster: "isarref" 

1315 
%%% End: 