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

7981

373 
applying setup functions from $text$, which refers to an ML expression of


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


375 
canonical way to initialize objectlogic specific tools and packages written


376 
in ML.

7167

377 
\end{descr}

7134

378 


379 

7981

380 
%FIXME remove!?


381 
%\subsection{Syntax translation functions}

7134

382 

7981

383 
%\indexisarcmd{parseasttranslation}\indexisarcmd{parsetranslation}


384 
%\indexisarcmd{printtranslation}\indexisarcmd{typedprinttranslation}


385 
%\indexisarcmd{printasttranslation}\indexisarcmd{tokentranslation}


386 
%\begin{matharray}{rcl}


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


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


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


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


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


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


393 
%\end{matharray}

7134

394 

7981

395 
%Syntax translation functions written in ML admit almost arbitrary


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


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


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


399 
%transformations.

7134

400 


401 


402 
\subsection{Oracles}


403 


404 
\indexisarcmd{oracle}


405 
\begin{matharray}{rcl}


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


407 
\end{matharray}


408 

7175

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


410 
control completely  each theorem carries a derivation object recording any


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


412 

7134

413 
\begin{rail}


414 
'oracle' name '=' text comment?


415 
;


416 
\end{rail}


417 

7167

418 
\begin{descr}

7175

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

7315

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

7335

421 
Object\mathord.T \to term$.

7167

422 
\end{descr}

7134

423 


424 


425 
\section{Proof commands}


426 

7315

427 
Proof commands provide transitions of Isar/VM machine configurations, which


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

7335

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


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


431 
modes of operation:

7167

432 
\begin{descr}


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


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

7895

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

7167

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

7175

437 
augmented by \emph{stating} additional assumptions, intermediate result etc.

7895

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

7458

439 
$proof(prove)$: existing facts (i.e.\ the contents of $this$) have been just

7895

440 
picked up in order to be used when refining the goal claimed next.

7167

441 
\end{descr}

7134

442 

7167

443 

7895

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

7167

445 

7895

446 
\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsect}


447 
\indexisarcmd{txt}\indexisarcmd{txtraw}

7134

448 
\begin{matharray}{rcl}

7167

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


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


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


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

7895

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

7134

454 
\end{matharray}


455 

7895

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


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


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


459 


460 
\railalias{txtraw}{txt\_raw}


461 
\railterm{txtraw}

7175

462 

7134

463 
\begin{rail}

7895

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

7134

465 
;


466 
\end{rail}


467 


468 

7315

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

7134

470 

7315

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

7134

472 
\begin{matharray}{rcl}


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


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


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


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


477 
\end{matharray}


478 

7315

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


480 
former closely correspond to Skolem constants, or metalevel universal


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


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

7319

483 
a local object that may be used in the subsequent proof as any other variable

7895

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


485 
current context will be universally closed wrt.\ $x$ at the outermost level:


486 
$\edrv \All x \phi$; this is expressed using Isabelle's metavariables.

7315

487 


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


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

7895

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


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


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


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


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


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


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


497 
user.

7315

498 

7319

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


500 
combining $\FIX x$ with another kind of assumption that causes any

7895

501 
hypothetical equation $x \equiv t$ to be eliminated by reflexivity. Thus,


502 
exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$.

7175

503 

7134

504 
\begin{rail}

7431

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

7134

506 
;

7315

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

7134

508 
;

7175

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

7134

510 
;


511 


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


513 
;

7458

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

7431

515 
;

7315

516 
assm: thmdecl? (prop proppat? +)


517 
;

7134

518 
\end{rail}


519 

7167

520 
\begin{descr}

7315

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


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

7335

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

7895

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

7335

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


526 
leaves $\Phi$ as new subgoals.


527 


528 
Several lists of assumptions may be given (separated by

7895

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


530 
these concatenated.

7315

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


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

7335

533 
$\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\PRESUME{}{x \equiv t}$, with the


534 
resulting hypothetical equation solved by reflexivity.

7431

535 


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

7167

537 
\end{descr}


538 

7895

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


540 
current context as a list of theorems.

7315

541 

7167

542 


543 
\subsection{Facts and forward chaining}


544 


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


546 
\begin{matharray}{rcl}


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


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


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


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


551 
\end{matharray}


552 

7319

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

7335

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


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


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

7458

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

7167

558 
\begin{rail}


559 
'note' thmdef? thmrefs comment?


560 
;


561 
'then' comment?


562 
;


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


564 
;


565 
\end{rail}


566 


567 
\begin{descr}

7175

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


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


570 
right hand sides.

7167

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

7895

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


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


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


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


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


577 
state before operation.

7335

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

7458

579 
equivalent to $\FROM{this}$.

7175

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


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

7167

582 
\end{descr}


583 

7389

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

7895

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


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

7458

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

7895

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


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

7389

590 

7167

591 


592 
\subsection{Goal statements}


593 


594 
\indexisarcmd{theorem}\indexisarcmd{lemma}


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


596 
\begin{matharray}{rcl}


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


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


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


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


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


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


603 
\end{matharray}


604 

7175

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

7895

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


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


608 
some pending goal and whether forward chaining is employed.

7175

609 

7167

610 
\begin{rail}


611 
('theorem'  'lemma') goal


612 
;


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


614 
;


615 


616 
goal: thmdecl? proppat comment?


617 
;


618 
\end{rail}


619 


620 
\begin{descr}

7335

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

7895

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

7167

623 
\item [$\LEMMANAME$] is similar to $\THEOREMNAME$, but tags the result as


624 
``lemma''.

7335

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

7167

626 
theorem with the current assumption context as hypotheses.

7335

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

7895

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


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


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


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


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


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


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

7167

635 
\end{descr}


636 


637 


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


639 

7175

640 
\indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by}


641 
\indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry}


642 
\begin{matharray}{rcl}


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


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


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


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


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


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


649 
\end{matharray}


650 

7335

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


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

7167

653 
\begin{enumerate}

7175

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

7335

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

7895

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

7167

657 

7335

658 
\item A \emph{terminal} conclusion step $\QED{m@2}$ solves any remaining goals


659 
completely. No facts are passed to $m@2$.

7167

660 
\end{enumerate}


661 

7335

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


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

7167

664 

7175

665 
\medskip


666 

7167

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

7895

668 
or constitute some wellunderstood reduction to new subgoals. Arbitrary


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


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


671 
way. A much better technique would be to $\SHOWNAME$ some nontrivial


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


673 
method, and then applied to some pending goal.

7167

674 

7175

675 
\medskip


676 


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


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

7458

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

7895

680 
separate default terminal method; in any case the final step is to solve all


681 
remaining goals by assumption, though.

7167

682 


683 
\begin{rail}


684 
'proof' interest? meth? comment?


685 
;


686 
'qed' meth? comment?


687 
;


688 
'by' meth meth? comment?


689 
;


690 
('.'  '..'  'sorry') comment?


691 
;


692 


693 
meth: method interest?


694 
;


695 
\end{rail}


696 


697 
\begin{descr}

7335

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


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


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

7895

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


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


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


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


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


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


707 
context. Debugging such a situation might involve temporarily changing


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


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


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


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


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


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

7175

714 
sufficient to see what is going wrong.

7895

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


716 
abbreviates $\BY{default}$.


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


718 
abbreviates $\BY{assumption}$.


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


720 
provided that \texttt{quick_and_dirty} is enabled, $\isarkeyword{sorry}$


721 
pretends to solve the goal without further ado. Of course, the result is a


722 
fake theorem only, involving some oracle in its internal derivation object


723 
(this is indicated as ``$[!]$'' in the printed result). The main


724 
application of $\isarkeyword{sorry}$ is to support experimentation and


725 
topdown proof development.

7167

726 
\end{descr}

7134

727 


728 

7315

729 
\subsection{Improper proof steps}


730 


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


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

7895

733 
come in handy for interactive exploration and debugging.

7315

734 


735 
\indexisarcmd{apply}\indexisarcmd{thenapply}\indexisarcmd{back}


736 
\begin{matharray}{rcl}


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


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


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


740 
\end{matharray}


741 


742 
\railalias{thenapply}{then\_apply}


743 
\railterm{thenapply}


744 


745 
\begin{rail}


746 
'apply' method


747 
;


748 
thenapply method


749 
;


750 
'back'


751 
;


752 
\end{rail}


753 


754 
\begin{descr}

7895

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


756 
tactic sense. Facts for forward chaining are reset.

7335

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

7510

758 
but keeps the goal's facts.

7315

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

7389

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


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


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

7315

763 
\end{descr}


764 


765 


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


767 


768 
\indexisarcmd{let}


769 
\begin{matharray}{rcl}


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


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


772 
\end{matharray}


773 


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


775 
or by annotating assumptions or goal statements ($\ASSUMENAME$, $\SHOWNAME$

7895

776 
etc.) with a list of patterns $\ISS{p@1 \dots}{p@n}$. In both cases,


777 
higherorder matching is invoked to bind extralogical term variables, which

7466

778 
may be either named schematic variables of the form $\Var{x}$, or nameless


779 
dummies ``\texttt{_}'' (underscore).\indexisarvar{_@\texttt{_}} Note that in


780 
the $\LETNAME$ form the patterns occur on the lefthand side, while the


781 
$\ISNAME$ patterns are in postfix position.

7315

782 

7319

783 
Term abbreviations are quite different from actual local definitions as


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

7315

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


786 
during the input process just after type checking.


787 


788 
\begin{rail}


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


790 
;


791 
\end{rail}


792 


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


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


795 


796 
\begin{descr}


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


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


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


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


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


802 
\end{descr}


803 

7319

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

7335

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

7466

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


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


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

7335

809 
objectlogical statement. The latter two abstract over any metalevel

7466

810 
parameters bound by $\Forall$.

7315

811 

7466

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


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


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


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


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

7895

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

7466

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


819 
this feature are calculational proofs (see \S\ref{sec:calculation}).

7315

820 


821 

7134

822 
\subsection{Block structure}


823 

7397

824 
\indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}}


825 
\begin{matharray}{rcl}


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

7974

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


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

7397

829 
\end{matharray}


830 

7167

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


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


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


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

7895

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


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


837 
effect of $\isarkeyword{next}$ is a local reset the proof


838 
context.\footnote{There is no goal focus involved here!}

7167

839 

7175

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

7895

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

7167

842 


843 
\begin{descr}


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

7895

845 
resetting the local context to the initial one.

7167

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

7895

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


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


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


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


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


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


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

7167

854 
\end{descr}

7134

855 


856 


857 
\section{Other commands}


858 


859 
\subsection{Diagnostics}


860 

7974

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

7134

862 
\begin{matharray}{rcl}

7974

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

7134

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


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

7974

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

7134

867 
\end{matharray}


868 

7335

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


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


871 
theory or proof configuration is not changed.


872 

7134

873 
\begin{rail}

7974

874 
'thm' thmrefs

7134

875 
;


876 
'term' term


877 
;


878 
'prop' prop


879 
;

7974

880 
'typ' type

7134

881 
;


882 
\end{rail}


883 

7167

884 
\begin{descr}

7974

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


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


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


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


889 
$thms$ do not have any permanent effect.

7895

890 
\item [$\isarkeyword{term}~t$, $\isarkeyword{prop}~\phi$] read, typechecks


891 
and print terms or propositions according to the current theory or proof


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


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


894 
abbreviations.

7974

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


896 
according to the current theory or proof context.

7167

897 
\end{descr}

7134

898 


899 


900 
\subsection{System operations}


901 

7167

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


903 
\indexisarcmd{updatethy}\indexisarcmd{updatethyonly}

7134

904 
\begin{matharray}{rcl}


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


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


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


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


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


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


911 
\end{matharray}


912 

7167

913 
\begin{descr}

7134

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


915 
process.


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

7175

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


918 
$\isarkeyword{update_thy}$, and $\isarkeyword{update_thy_only}$] load some

7895

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


920 
the corresponding ML functions\footnote{For historic reasons, the original


921 
ML versions also change the theory context to that of the theory loaded.}


922 
(see also \cite[\S1,\S6]{isabelleref}). Note that both the ML and Isar


923 
versions may load new and oldstyle theories alike.

7167

924 
\end{descr}

7134

925 

7895

926 
Note that these system commands are scarcely used when working with the


927 
Proof~General interface, since loading of theories is done fully


928 
transparently.

7134

929 

7046

930 
%%% Local Variables:


931 
%%% mode: latex


932 
%%% TeXmaster: "isarref"


933 
%%% End:
