7046

1 

7895

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

7167

3 

7315

4 
Subsequently, we introduce the main part of the basic Isar theory and proof


5 
commands as provided by Isabelle/Pure. Chapter~\ref{ch:gentools} describes

7895

6 
further Isar elements provided by generic tools and packages (such as the


7 
Simplifier) that are either part of Pure Isabelle or preloaded by most object


8 
logics. Chapter~\ref{ch:holtools} refers to actual objectlogic specific


9 
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


20 
proving, which facilitates porting of legacy proof scripts.

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} \\

7134

30 
\isarcmd{theory} & : & \isartrans{\cdot}{theory} \\


31 
\isarcmd{context}^* & : & \isartrans{\cdot}{theory} \\


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


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


48 
last command in a 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


65 
the formal begin of a theory. In actual document preparation the


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}

7981

131 
package to be included in {\LaTeX}.}

7167

132 
\end{descr}

7134

133 

7895

134 
Any markup command (except $\isarkeyword{text_raw}$) corresponds to a {\LaTeX}

7981

135 
macro with the name prefixed by \verb,\isamarkup, (e.g.\

7895

136 
\verb,\isamarkupchapter, for $\isarkeyword{chapter}$). The \railqtoken{text}

7981

137 
argument is passed to that macro unchanged, i.e.\ further {\LaTeX} commands


138 
may be included here as well.

7895

139 

7981

140 
\medskip Additional markup commands are available for proofs (see

7895

141 
\S\ref{sec:markupprf}). Also note that the $\isarkeyword{header}$


142 
declaration (see \S\ref{sec:beginthy}) admits to insert document markup


143 
elements just preceding the actual theory definition.


144 

7134

145 

7135

146 
\subsection{Type classes and sorts}\label{sec:classes}

7134

147 


148 
\indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort}


149 
\begin{matharray}{rcl}


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


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


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


153 
\end{matharray}


154 


155 
\begin{rail}

7167

156 
'classes' (classdecl comment? +)

7134

157 
;


158 
'classrel' nameref '<' nameref comment?


159 
;


160 
'defaultsort' sort comment?


161 
;


162 
\end{rail}


163 

7167

164 
\begin{descr}

7335

165 
\item [$\isarkeyword{classes}~c<\vec c$] declares class $c$ to be a subclass


166 
of existing classes $\vec c$. Cyclic class structures are ruled out.

7134

167 
\item [$\isarkeyword{classrel}~c@1<c@2$] states a subclass relation between


168 
existing classes $c@1$ and $c@2$. This is done axiomatically! The

7895

169 
$\isarkeyword{instance}$ command (see \S\ref{sec:axclass}) provides a way to

7175

170 
introduce proven class relations.

7134

171 
\item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for

7895

172 
any type variables given without sort constraints. Usually, the default

7134

173 
sort would be only changed when defining new logics.

7167

174 
\end{descr}

7134

175 


176 

7315

177 
\subsection{Primitive types and type abbreviations}\label{sec:typespure}

7134

178 


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


180 
\begin{matharray}{rcl}


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


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


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


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


185 
\end{matharray}


186 


187 
\begin{rail}


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


189 
;


190 
'typedecl' typespec infix? comment?


191 
;


192 
'nonterminals' (name +) comment?


193 
;


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


195 
;


196 
\end{rail}


197 

7167

198 
\begin{descr}

7335

199 
\item [$\TYPES~(\vec\alpha)t = \tau$] introduces \emph{type synonym}

7134

200 
$(\vec\alpha)t$ for existing type $\tau$. Unlike actual type definitions,


201 
as are available in Isabelle/HOL for example, type synonyms are just purely

7895

202 
syntactic abbreviations without any logical significance. Internally, type

7981

203 
synonyms are fully expanded.

7134

204 
\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] declares a new type constructor

7895

205 
$t$, intended as an actual logical type. Note that objectlogics such as


206 
Isabelle/HOL override $\isarkeyword{typedecl}$ by their own version.

7175

207 
\item [$\isarkeyword{nonterminals}~\vec c$] declares $0$ary type constructors


208 
$\vec c$ to act as purely syntactic types, i.e.\ nonterminal symbols of


209 
Isabelle's inner syntax of terms or types.

7335

210 
\item [$\isarkeyword{arities}~t::(\vec s)s$] augments Isabelle's ordersorted


211 
signature of types by new type constructor arities. This is done


212 
axiomatically! The $\isarkeyword{instance}$ command (see

7895

213 
\S\ref{sec:axclass}) provides a way to introduce proven type arities.

7167

214 
\end{descr}

7134

215 


216 

7981

217 
\subsection{Constants and simple definitions}\label{sec:consts}

7134

218 

7175

219 
\indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}\indexoutertoken{constdecl}

7134

220 
\begin{matharray}{rcl}


221 
\isarcmd{consts} & : & \isartrans{theory}{theory} \\


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


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


224 
\end{matharray}


225 


226 
\begin{rail}


227 
'consts' (constdecl +)


228 
;

7608

229 
'defs' (axmdecl prop comment? +)

7134

230 
;


231 
'constdefs' (constdecl prop comment? +)


232 
;


233 


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


235 
;


236 
\end{rail}


237 

7167

238 
\begin{descr}

7335

239 
\item [$\CONSTS~c::\sigma$] declares constant $c$ to have any instance of type


240 
scheme $\sigma$. The optional mixfix annotations may attach concrete syntax

7895

241 
to the constants declared.

7335

242 
\item [$\DEFS~name: eqn$] introduces $eqn$ as a definitional axiom for some


243 
existing constant. See \cite[\S6]{isabelleref} for more details on the


244 
form of equations admitted as constant definitions.


245 
\item [$\isarkeyword{constdefs}~c::\sigma~eqn$] combines declarations and


246 
definitions of constants, using canonical name $c_def$ for the definitional


247 
axiom.

7167

248 
\end{descr}

7134

249 


250 

7981

251 
\subsection{Syntax and translations}\label{sec:syntrans}

7134

252 


253 
\indexisarcmd{syntax}\indexisarcmd{translations}


254 
\begin{matharray}{rcl}


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


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


257 
\end{matharray}


258 


259 
\begin{rail}


260 
'syntax' ('(' name 'output'? ')')? (constdecl +)


261 
;


262 
'translations' (transpat ('=='  '=>'  '<=') transpat comment? +)


263 
;


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


265 
;


266 
\end{rail}


267 

7167

268 
\begin{descr}

7175

269 
\item [$\isarkeyword{syntax}~(mode)~decls$] is similar to $\CONSTS~decls$,


270 
except that the actual logical signature extension is omitted. Thus the


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

7335

272 
arbitrary ways, independently of the logic. The $mode$ argument refers to


273 
the print mode that the grammar rules belong; unless there is the


274 
\texttt{output} flag given, all productions are added both to the input and


275 
output grammar.

7175

276 
\item [$\isarkeyword{translations}~rules$] specifies syntactic translation

7981

277 
rules (i.e.\ \emph{macros}): parse~/ print rules (\texttt{==}), parse rules

7895

278 
(\texttt{=>}), or print rules (\texttt{<=}). Translation patterns may be


279 
prefixed by the syntactic category to be used for parsing; the default is

7134

280 
\texttt{logic}.

7167

281 
\end{descr}

7134

282 


283 


284 
\subsection{Axioms and theorems}


285 


286 
\indexisarcmd{axioms}\indexisarcmd{theorems}\indexisarcmd{lemmas}


287 
\begin{matharray}{rcl}


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


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


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


291 
\end{matharray}


292 


293 
\begin{rail}

7135

294 
'axioms' (axmdecl prop comment? +)

7134

295 
;


296 
('theorems'  'lemmas') thmdef? thmrefs


297 
;


298 
\end{rail}


299 

7167

300 
\begin{descr}

7335

301 
\item [$\isarkeyword{axioms}~a: \phi$] introduces arbitrary statements as

7895

302 
axioms of the metalogic. In fact, axioms are ``axiomatic theorems'', and


303 
may be referred later just as any other theorem.

7134

304 


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

7175

306 
Everyday work is typically done the hard way, with proper definitions and

7134

307 
actual theorems.

7335

308 
\item [$\isarkeyword{theorems}~a = \vec b$] stores lists of existing theorems.

7981

309 
Typical applications would also involve attributes, to augment the

7335

310 
Simplifier context, for example.

7134

311 
\item [$\isarkeyword{lemmas}$] is similar to $\isarkeyword{theorems}$, but


312 
tags the results as ``lemma''.

7167

313 
\end{descr}

7134

314 


315 

7167

316 
\subsection{Name spaces}

7134

317 

7167

318 
\indexisarcmd{global}\indexisarcmd{local}

7134

319 
\begin{matharray}{rcl}


320 
\isarcmd{global} & : & \isartrans{theory}{theory} \\


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


322 
\end{matharray}


323 

7895

324 
Isabelle organizes any kind of name declarations (of types, constants,


325 
theorems etc.) by hierarchically structured name spaces. Normally the user


326 
never has to control the behavior of name space entry by hand, yet the


327 
following commands provide some way to do so.

7175

328 

7167

329 
\begin{descr}


330 
\item [$\isarkeyword{global}$ and $\isarkeyword{local}$] change the current


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


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

7895

333 
Changing this to $\isarkeyword{global}$ causes all names to be declared


334 
without the theory prefix, until $\isarkeyword{local}$ is declared again.

7167

335 
\end{descr}

7134

336 


337 

7167

338 
\subsection{Incorporating ML code}\label{sec:ML}

7134

339 

7895

340 
\indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{MLsetup}\indexisarcmd{setup}

7134

341 
\begin{matharray}{rcl}


342 
\isarcmd{use} & : & \isartrans{\cdot}{\cdot} \\


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

7895

344 
\isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\

7175

345 
\isarcmd{setup} & : & \isartrans{theory}{theory} \\

7134

346 
\end{matharray}


347 

7895

348 
\railalias{MLsetup}{ML\_setup}


349 
\railterm{MLsetup}


350 

7134

351 
\begin{rail}


352 
'use' name


353 
;

7895

354 
('ML'  MLsetup  'setup') text

7134

355 
;


356 
\end{rail}


357 

7167

358 
\begin{descr}

7175

359 
\item [$\isarkeyword{use}~file$] reads and executes ML commands from $file$.

7466

360 
The current theory context (if present) is passed down to the ML session,

7981

361 
but may not be modified. Furthermore, the file name is checked with the

7466

362 
$\isarkeyword{files}$ dependency declaration given in the theory header (see


363 
also \S\ref{sec:beginthy}).


364 

7895

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


366 
context is passed in the same way as for $\isarkeyword{use}$.


367 


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


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


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


371 

7167

372 
\item [$\isarkeyword{setup}~text$] changes the current theory context by

7987

373 
applying $text$, which refers to an ML expression of type $(theory \to


374 
theory)~list$. The $\isarkeyword{setup}$ command is the canonical way to


375 
initialize objectlogic specific tools and packages written in ML.

7167

376 
\end{descr}

7134

377 


378 

7981

379 
%FIXME remove!?


380 
%\subsection{Syntax translation functions}

7134

381 

7981

382 
%\indexisarcmd{parseasttranslation}\indexisarcmd{parsetranslation}


383 
%\indexisarcmd{printtranslation}\indexisarcmd{typedprinttranslation}


384 
%\indexisarcmd{printasttranslation}\indexisarcmd{tokentranslation}


385 
%\begin{matharray}{rcl}


386 
% \isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\


387 
% \isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\


388 
% \isarcmd{print_translation} & : & \isartrans{theory}{theory} \\


389 
% \isarcmd{typed_print_translation} & : & \isartrans{theory}{theory} \\


390 
% \isarcmd{print_ast_translation} & : & \isartrans{theory}{theory} \\


391 
% \isarcmd{token_translation} & : & \isartrans{theory}{theory} \\


392 
%\end{matharray}

7134

393 

7981

394 
%Syntax translation functions written in ML admit almost arbitrary


395 
%manipulations of Isabelle's inner syntax. Any of the above commands have a


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


397 
%appropriate type. See \cite[\S8]{isabelleref} for more information on syntax


398 
%transformations.

7134

399 


400 


401 
\subsection{Oracles}


402 


403 
\indexisarcmd{oracle}


404 
\begin{matharray}{rcl}


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


406 
\end{matharray}


407 

7175

408 
Oracles provide an interface to external reasoning systems, without giving up


409 
control completely  each theorem carries a derivation object recording any


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


411 

7134

412 
\begin{rail}


413 
'oracle' name '=' text comment?


414 
;


415 
\end{rail}


416 

7167

417 
\begin{descr}

7175

418 
\item [$\isarkeyword{oracle}~name=text$] declares oracle $name$ to be ML

7315

419 
function $text$, which has to be of type $Sign\mathord.sg \times

7335

420 
Object\mathord.T \to term$.

7167

421 
\end{descr}

7134

422 


423 


424 
\section{Proof commands}


425 

7987

426 
Proof commands perform transitions of Isar/VM machine configurations, which

7315

427 
are blockstructured, consisting of a stack of nodes with three main

7335

428 
components: logical proof context, current facts, and open goals. Isar/VM


429 
transitions are \emph{typed} according to the following three three different


430 
modes of operation:

7167

431 
\begin{descr}


432 
\item [$proof(prove)$] means that a new goal has just been stated that is now


433 
to be \emph{proven}; the next command may refine it by some proof method

7895

434 
(read: tactic), and enter a subproof to establish the actual result.

7167

435 
\item [$proof(state)$] is like an internal theory mode: the context may be

7987

436 
augmented by \emph{stating} additional assumptions, intermediate results


437 
etc.

7895

438 
\item [$proof(chain)$] is intermediate between $proof(state)$ and

7987

439 
$proof(prove)$: existing facts (i.e.\ the contents of the special ``$this$''


440 
register) have been just picked up in order to be used when refining the


441 
goal claimed next.

7167

442 
\end{descr}

7134

443 

7167

444 

7895

445 
\subsection{Proof markup commands}\label{sec:markupprf}

7167

446 

7987

447 
\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect}

7895

448 
\indexisarcmd{txt}\indexisarcmd{txtraw}

7134

449 
\begin{matharray}{rcl}

7167

450 
\isarcmd{sect} & : & \isartrans{proof(state)}{proof(state)} \\


451 
\isarcmd{subsect} & : & \isartrans{proof(state)}{proof(state)} \\


452 
\isarcmd{subsubsect} & : & \isartrans{proof(state)}{proof(state)} \\


453 
\isarcmd{txt} & : & \isartrans{proof(state)}{proof(state)} \\

7895

454 
\isarcmd{txt_raw} & : & \isartrans{proof(state)}{proof(state)} \\

7134

455 
\end{matharray}


456 

7895

457 
These markup commands for proof mode closely correspond to the ones of theory


458 
mode (see \S\ref{sec:markupthy}). Note that $\isarkeyword{txt_raw}$ is


459 
special in the same way as $\isarkeyword{text_raw}$.


460 


461 
\railalias{txtraw}{txt\_raw}


462 
\railterm{txtraw}

7175

463 

7134

464 
\begin{rail}

7895

465 
('sect'  'subsect'  'subsubsect'  'txt'  txtraw) text

7134

466 
;


467 
\end{rail}


468 


469 

7315

470 
\subsection{Proof context}\label{sec:proofcontext}

7134

471 

7315

472 
\indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def}

7134

473 
\begin{matharray}{rcl}


474 
\isarcmd{fix} & : & \isartrans{proof(state)}{proof(state)} \\


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


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


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


478 
\end{matharray}


479 

7315

480 
The logical proof context consists of fixed variables and assumptions. The


481 
former closely correspond to Skolem constants, or metalevel universal


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


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

7987

484 
a local value that may be used in the subsequent proof as any other variable

7895

485 
or constant. Furthermore, any result $\edrv \phi[x]$ exported from the

7987

486 
context will be universally closed wrt.\ $x$ at the outermost level: $\edrv


487 
\All x \phi$ (this is expressed using Isabelle's metavariables).

7315

488 


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


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

7895

491 
proof steps. On the other hand, any result $\chi \drv \phi$ exported from the


492 
context becomes conditional wrt.\ the assumption: $\edrv \chi \Imp \phi$.


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


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


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


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


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


498 
user.

7315

499 

7319

500 
Local definitions, introduced by $\DEF{}{x \equiv t}$, are achieved by

7987

501 
combining $\FIX x$ with another version of assumption that causes any


502 
hypothetical equation $x \equiv t$ to be eliminated by the reflexivity rule.


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

7175

504 

7134

505 
\begin{rail}

7431

506 
'fix' (vars + 'and') comment?

7134

507 
;

7315

508 
('assume'  'presume') (assm comment? + 'and')

7134

509 
;

7175

510 
'def' thmdecl? \\ var '==' term termpat? comment?

7134

511 
;


512 


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


514 
;

7458

515 
vars: (name+) ('::' type)?

7431

516 
;

7315

517 
assm: thmdecl? (prop proppat? +)


518 
;

7134

519 
\end{rail}


520 

7167

521 
\begin{descr}

7315

522 
\item [$\FIX{x}$] introduces a local \emph{arbitrary, but fixed} variable $x$.


523 
\item [$\ASSUME{a}{\Phi}$ and $\PRESUME{a}{\Phi}$] introduce local theorems

7335

524 
$\Phi$ by assumption. Subsequent results applied to an enclosing goal

7895

525 
(e.g.\ by $\SHOWNAME$) are handled as follows: $\ASSUMENAME$ expects to be

7335

526 
able to unify with existing premises in the goal, while $\PRESUMENAME$


527 
leaves $\Phi$ as new subgoals.


528 


529 
Several lists of assumptions may be given (separated by

7895

530 
$\isarkeyword{and}$); the resulting list of current facts consists of all of


531 
these concatenated.

7315

532 
\item [$\DEF{a}{x \equiv t}$] introduces a local (nonpolymorphic) definition.


533 
In results exported from the context, $x$ is replaced by $t$. Basically,

7987

534 
$\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\ASSUME{}{x \equiv t}$, with the

7335

535 
resulting hypothetical equation solved by reflexivity.

7431

536 


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

7167

538 
\end{descr}


539 

7895

540 
The special name $prems$\indexisarthm{prems} refers to all assumptions of the


541 
current context as a list of theorems.

7315

542 

7167

543 


544 
\subsection{Facts and forward chaining}


545 


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


547 
\begin{matharray}{rcl}


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


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


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


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


552 
\end{matharray}


553 

7319

554 
New facts are established either by assumption or proof of local statements.

7335

555 
Any fact will usually be involved in further proofs, either as explicit


556 
arguments of proof methods or when forward chaining towards the next goal via


557 
$\THEN$ (and variants). Note that the special theorem name

7987

558 
$this$\indexisarthm{this} refers to the most recently established facts.

7167

559 
\begin{rail}


560 
'note' thmdef? thmrefs comment?


561 
;


562 
'then' comment?


563 
;


564 
('from'  'with') thmrefs comment?


565 
;


566 
\end{rail}


567 


568 
\begin{descr}

7175

569 
\item [$\NOTE{a}{\vec b}$] recalls existing facts $\vec b$, binding the result


570 
as $a$. Note that attributes may be involved as well, both on the left and


571 
right hand sides.

7167

572 
\item [$\THEN$] indicates forward chaining by the current facts in order to

7895

573 
establish the goal to be claimed next. The initial proof method invoked to


574 
refine that will be offered the facts to do ``anything appropriate'' (cf.\


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


576 
\S\ref{sec:puremeth}) would typically do an elimination rather than an


577 
introduction. Automatic methods usually insert the facts into the goal


578 
state before operation.

7335

579 
\item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; thus $\THEN$ is

7458

580 
equivalent to $\FROM{this}$.

7175

581 
\item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~facts}$; thus the forward


582 
chaining is from earlier facts together with the current ones.

7167

583 
\end{descr}


584 

7389

585 
Basic proof methods (such as $rule$, see \S\ref{sec:puremeth}) expect

7895

586 
multiple facts to be given in their proper order, corresponding to a prefix of


587 
the premises of the rule involved. Note that positions may be easily skipped

7458

588 
using a form like $\FROM{\text{\texttt{_}}~a~b}$, for example. This involves

7895

589 
the trivial rule $\PROP\psi \Imp \PROP\psi$, which is bound in Isabelle/Pure


590 
as ``\texttt{_}'' (underscore).\indexisarthm{_@\texttt{_}}

7389

591 

7167

592 


593 
\subsection{Goal statements}


594 


595 
\indexisarcmd{theorem}\indexisarcmd{lemma}


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


597 
\begin{matharray}{rcl}


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


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

7987

600 
\isarcmd{have} & : & \isartrans{proof(state) ~~ proof(chain)}{proof(prove)} \\


601 
\isarcmd{show} & : & \isartrans{proof(state) ~~ proof(chain)}{proof(prove)} \\

7167

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


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


604 
\end{matharray}


605 

7175

606 
Proof mode is entered from theory mode by initial goal commands $\THEOREMNAME$

7895

607 
and $\LEMMANAME$. New local goals may be claimed within proof mode as well.


608 
Four variants are available, indicating whether the result is meant to solve

7987

609 
some pending goal or whether forward chaining is employed.

7175

610 

7167

611 
\begin{rail}


612 
('theorem'  'lemma') goal


613 
;


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


615 
;


616 


617 
goal: thmdecl? proppat comment?


618 
;


619 
\end{rail}


620 


621 
\begin{descr}

7335

622 
\item [$\THEOREM{a}{\phi}$] enters proof mode with $\phi$ as main goal,

7895

623 
eventually resulting in some theorem $\turn \phi$ put back into the theory.

7987

624 
\item [$\LEMMA{a}{\phi}$] is similar to $\THEOREMNAME$, but tags the result as

7167

625 
``lemma''.

7335

626 
\item [$\HAVE{a}{\phi}$] claims a local goal, eventually resulting in a

7167

627 
theorem with the current assumption context as hypotheses.

7335

628 
\item [$\SHOW{a}{\phi}$] is similar to $\HAVE{a}{\phi}$, but solves some

7895

629 
pending goal with the result \emph{exported} into the corresponding context


630 
(cf.\ \S\ref{sec:proofcontext}).


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


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


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


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


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

7167

636 
\end{descr}


637 


638 


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


640 

7175

641 
\indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by}


642 
\indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry}


643 
\begin{matharray}{rcl}


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


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


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


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


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


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


650 
\end{matharray}


651 

7335

652 
Arbitrary goal refinement via tactics is considered harmful. Consequently the


653 
Isar framework admits proof methods to be invoked in two places only.

7167

654 
\begin{enumerate}

7175

655 
\item An \emph{initial} refinement step $\PROOF{m@1}$ reduces a newly stated

7335

656 
goal to a number of subgoals that are to be solved later. Facts are passed

7895

657 
to $m@1$ for forward chaining, if so indicated by $proof(chain)$ mode.

7167

658 

7987

659 
\item A \emph{terminal} conclusion step $\QED{m@2}$ is intended to solve


660 
remaining goals. No facts are passed to $m@2$.

7167

661 
\end{enumerate}


662 

7335

663 
The only other proper way to affect pending goals is by $\SHOWNAME$ (or


664 
$\THUSNAME$), which involves an explicit statement of what is to be solved.

7167

665 

7175

666 
\medskip


667 

7167

668 
Also note that initial proof methods should either solve the goal completely,

7895

669 
or constitute some wellunderstood reduction to new subgoals. Arbitrary


670 
automatic proof tools that are prone leave a large number of badly structured


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

7987

672 
way.


673 
%FIXME


674 
%A more appropriate technique would be to $\SHOWNAME$ some nontrivial


675 
%reduction as an explicit rule, which is solved completely by some automated


676 
%method, and then applied to some pending goal.

7167

677 

7175

678 
\medskip


679 


680 
Unless given explicitly by the user, the default initial method is


681 
``$default$'', which is usually set up to apply a single standard elimination

7458

682 
or introduction rule according to the topmost symbol involved. There is no

7987

683 
separate default terminal method. In any case, any goals left after that are


684 
solved by assumption as the very last step.

7167

685 


686 
\begin{rail}


687 
'proof' interest? meth? comment?


688 
;


689 
'qed' meth? comment?


690 
;


691 
'by' meth meth? comment?


692 
;


693 
('.'  '..'  'sorry') comment?


694 
;


695 


696 
meth: method interest?


697 
;


698 
\end{rail}


699 


700 
\begin{descr}

7335

701 
\item [$\PROOF{m@1}$] refines the goal by proof method $m@1$; facts for


702 
forward chaining are passed if so indicated by $proof(chain)$ mode.


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

7895

704 
concludes the subproof by assumption. If the goal had been $\SHOWNAME$ (or


705 
$\THUSNAME$), some pending subgoal is solved as well by the rule resulting


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


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


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


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


710 
context. Debugging such a situation might involve temporarily changing


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


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


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

7987

714 
abbreviates $\PROOF{m@1}~\QED{m@2}$, with backtracking across both methods,


715 
though. Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done

7895

716 
by expanding its definition; in many cases $\PROOF{m@1}$ is already

7175

717 
sufficient to see what is going wrong.

7895

718 
\item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it


719 
abbreviates $\BY{default}$.


720 
\item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it


721 
abbreviates $\BY{assumption}$.


722 
\item [$\isarkeyword{sorry}$] is a \emph{fake proof}\index{proof!fake};

7987

723 
provided that the \texttt{quick_and_dirty} flag is enabled,


724 
$\isarkeyword{sorry}$ pretends to solve the goal without further ado. Of


725 
course, the result is a fake theorem only, involving some oracle in its


726 
internal derivation object (this is indicated as ``$[!]$'' in the printed


727 
result). The main application of $\isarkeyword{sorry}$ is to support


728 
experimentation and topdown proof development.

7167

729 
\end{descr}

7134

730 


731 

7315

732 
\subsection{Improper proof steps}


733 


734 
The following commands emulate unstructured tactic scripts to some extent.


735 
While these are anathema for writing proper Isar proof documents, they might

7895

736 
come in handy for interactive exploration and debugging.

7315

737 


738 
\indexisarcmd{apply}\indexisarcmd{thenapply}\indexisarcmd{back}


739 
\begin{matharray}{rcl}


740 
\isarcmd{apply}^* & : & \isartrans{proof}{proof} \\


741 
\isarcmd{then_apply}^* & : & \isartrans{proof}{proof} \\


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


743 
\end{matharray}


744 


745 
\railalias{thenapply}{then\_apply}


746 
\railterm{thenapply}


747 


748 
\begin{rail}


749 
'apply' method


750 
;


751 
thenapply method


752 
;


753 
'back'


754 
;


755 
\end{rail}


756 


757 
\begin{descr}

7895

758 
\item [$\isarkeyword{apply}~(m)$] applies proof method $m$ in the plain old


759 
tactic sense. Facts for forward chaining are reset.

7335

760 
\item [$\isarkeyword{then_apply}~(m)$] is similar to $\isarkeyword{apply}$,

7510

761 
but keeps the goal's facts.

7315

762 
\item [$\isarkeyword{back}$] does backtracking over the result sequence of

7389

763 
the latest proof command.\footnote{Unlike the ML function \texttt{back}


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


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

7315

766 
\end{descr}


767 


768 


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


770 


771 
\indexisarcmd{let}


772 
\begin{matharray}{rcl}


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


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


775 
\end{matharray}


776 


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

7987

778 
or by annotating assumptions or goal statements with a list of patterns


779 
$\ISS{p@1\;\dots}{p@n}$. In both cases, higherorder matching is invoked to


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


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


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


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


784 
postfix position.

7315

785 

7319

786 
Term abbreviations are quite different from actual local definitions as


787 
introduced via $\DEFNAME$ (see \S\ref{sec:proofcontext}). The latter are

7315

788 
visible within the logic as actual equations, while abbreviations disappear


789 
during the input process just after type checking.


790 


791 
\begin{rail}


792 
'let' ((term + 'as') '=' term comment? + 'and')


793 
;


794 
\end{rail}


795 


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


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


798 


799 
\begin{descr}


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


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


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


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


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


805 
\end{descr}


806 

7319

807 
A few \emph{automatic} term abbreviations\index{automatic abbreviation} for

7335

808 
goals and facts are available as well. For any open goal,

7466

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


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


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

7335

812 
objectlogical statement. The latter two abstract over any metalevel

7987

813 
parameters.

7315

814 

7466

815 
Fact statements resulting from assumptions or finished goals are bound as


816 
$\Var{this_prop}$\indexisarvar{thisprop},


817 
$\Var{this_concl}$\indexisarvar{thisconcl}, and


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


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

7895

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

7466

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

7987

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

7315

823 


824 

7134

825 
\subsection{Block structure}


826 

7397

827 
\indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}}


828 
\begin{matharray}{rcl}


829 
\isarcmd{next} & : & \isartrans{proof(state)}{proof(state)} \\

7974

830 
\BG & : & \isartrans{proof(state)}{proof(state)} \\


831 
\EN & : & \isartrans{proof(state)}{proof(state)} \\

7397

832 
\end{matharray}


833 

7167

834 
While Isar is inherently blockstructured, opening and closing blocks is


835 
mostly handled rather casually, with little explicit userintervention. Any


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


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

7895

838 
different context within a subproof may be switched via $\isarkeyword{next}$,


839 
which is just a single blockclose followed by blockopen again. Thus the

7987

840 
effect of $\isarkeyword{next}$ to reset the local proof context. There is no


841 
goal focus involved here!

7167

842 

7175

843 
For slightly more advanced applications, there are explicit block parentheses

7895

844 
as well. These typically achieve a stronger forward style of reasoning.

7167

845 


846 
\begin{descr}


847 
\item [$\isarkeyword{next}$] switches to a fresh block within a subproof,

7895

848 
resetting the local context to the initial one.

7167

849 
\item [$\isarkeyword{\{\{}$ and $\isarkeyword{\}\}}$] explicitly open and

7895

850 
close blocks. Any current facts pass through ``$\isarkeyword{\{\{}$''


851 
unchanged, while ``$\isarkeyword{\}\}}$'' causes any result to be


852 
\emph{exported} into the enclosing context. Thus fixed variables are


853 
generalized, assumptions discharged, and local definitions unfolded (cf.\


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


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


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

7167

857 
\end{descr}

7134

858 


859 


860 
\section{Other commands}


861 


862 
\subsection{Diagnostics}


863 

7974

864 
\indexisarcmd{thm}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{typ}

7134

865 
\begin{matharray}{rcl}

7974

866 
\isarcmd{thm} & : & \isarkeep{theory~~proof} \\

7134

867 
\isarcmd{term} & : & \isarkeep{theory~~proof} \\


868 
\isarcmd{prop} & : & \isarkeep{theory~~proof} \\

7974

869 
\isarcmd{typ} & : & \isarkeep{theory~~proof} \\

7134

870 
\end{matharray}


871 

7335

872 
These commands are not part of the actual Isabelle/Isar syntax, but assist


873 
interactive development. Also note that $undo$ does not apply here, since the


874 
theory or proof configuration is not changed.


875 

7134

876 
\begin{rail}

7974

877 
'thm' thmrefs

7134

878 
;


879 
'term' term


880 
;


881 
'prop' prop


882 
;

7974

883 
'typ' type

7134

884 
;


885 
\end{rail}


886 

7167

887 
\begin{descr}

7974

888 
\item [$\isarkeyword{thm}~thms$] retrieves lists of theorems from the current


889 
theory or proof context. Note that any attributes included in the theorem


890 
specifications are applied to a temporary context derived from the current


891 
theory or proof; the result is discarded, i.e.\ attributes involved in


892 
$thms$ do not have any permanent effect.

7987

893 
\item [$\isarkeyword{term}~t$, $\isarkeyword{prop}~\phi$] read, typecheck and


894 
print terms or propositions according to the current theory or proof

7895

895 
context; the inferred type of $t$ is output as well. Note that these


896 
commands are also useful in inspecting the current environment of term


897 
abbreviations.

7974

898 
\item [$\isarkeyword{typ}~\tau$] reads and prints types of the metalogic


899 
according to the current theory or proof context.

7167

900 
\end{descr}

7134

901 


902 


903 
\subsection{System operations}


904 

7167

905 
\indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{usethy}\indexisarcmd{usethyonly}


906 
\indexisarcmd{updatethy}\indexisarcmd{updatethyonly}

7134

907 
\begin{matharray}{rcl}


908 
\isarcmd{cd} & : & \isarkeep{\cdot} \\


909 
\isarcmd{pwd} & : & \isarkeep{\cdot} \\


910 
\isarcmd{use_thy} & : & \isarkeep{\cdot} \\


911 
\isarcmd{use_thy_only} & : & \isarkeep{\cdot} \\


912 
\isarcmd{update_thy} & : & \isarkeep{\cdot} \\


913 
\isarcmd{update_thy_only} & : & \isarkeep{\cdot} \\


914 
\end{matharray}


915 

7167

916 
\begin{descr}

7134

917 
\item [$\isarkeyword{cd}~name$] changes the current directory of the Isabelle


918 
process.


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

7175

920 
\item [$\isarkeyword{use_thy}$, $\isarkeyword{use_thy_only}$,

7987

921 
$\isarkeyword{update_thy}$, $\isarkeyword{update_thy_only}$] load some

7895

922 
theory given as $name$ argument. These commands are basically the same as

7987

923 
the corresponding ML functions\footnote{The ML versions also change the


924 
implicit theory context to that of the theory loaded.} (see also


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


926 
load new and oldstyle theories alike.

7167

927 
\end{descr}

7134

928 

7987

929 
These system commands are scarcely used when working with the Proof~General


930 
interface, since loading of theories is done fully transparently.

7134

931 

7046

932 
%%% Local Variables:


933 
%%% mode: latex


934 
%%% TeXmaster: "isarref"


935 
%%% End:
