author  webertj 
Tue, 18 Jul 2006 14:53:27 +0200  
changeset 20143  54e493016486 
parent 19792  e8e3da6d3ff7 
child 20212  f4a8b4e2fb29 
permissions  rwrr 
9932  1 
(*<*) 
16417  2 
theory simp imports Main begin 
9932  3 
(*>*) 
9922  4 

11214  5 
subsection{*Simplification Rules*} 
9932  6 

11458  7 
text{*\index{simplification rules} 
8 
To facilitate simplification, 

9 
the attribute @{text"[simp]"}\index{*simp (attribute)} 

10 
declares theorems to be simplification rules, which the simplifier 

11 
will use automatically. In addition, \isacommand{datatype} and 

12 
\isacommand{primrec} declarations (and a few others) 

13 
implicitly declare some simplification rules. 

14 
Explicit definitions are \emph{not} declared as 

9932  15 
simplification rules automatically! 
16 

11458  17 
Nearly any theorem can become a simplification 
18 
rule. The simplifier will try to transform it into an equation. 

19 
For example, the theorem 

20 
@{prop"~P"} is turned into @{prop"P = False"}. The details 

9932  21 
are explained in \S\ref{sec:SimpHow}. 
22 

11458  23 
The simplification attribute of theorems can be turned on and off:% 
12489  24 
\index{*simp del (attribute)} 
9932  25 
\begin{quote} 
26 
\isacommand{declare} \textit{theoremname}@{text"[simp]"}\\ 

27 
\isacommand{declare} \textit{theoremname}@{text"[simp del]"} 

28 
\end{quote} 

11309  29 
Only equations that really simplify, like \isa{rev\ 
30 
{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs} and 

31 
\isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ 

32 
{\isacharequal}\ xs}, should be declared as default simplification rules. 

33 
More specific ones should only be used selectively and should 

34 
not be made default. Distributivity laws, for example, alter 

35 
the structure of terms and can produce an exponential blowup instead of 

36 
simplification. A default simplification rule may 

37 
need to be disabled in certain proofs. Frequent changes in the simplification 

38 
status of a theorem may indicate an unwise use of defaults. 

9932  39 
\begin{warn} 
11458  40 
Simplification can run forever, for example if both $f(x) = g(x)$ and 
9932  41 
$g(x) = f(x)$ are simplification rules. It is the user's responsibility not 
42 
to include simplification rules that can lead to nontermination, either on 

43 
their own or in combination with other simplification rules. 

44 
\end{warn} 

12332  45 
\begin{warn} 
46 
It is inadvisable to toggle the simplification attribute of a 

47 
theorem from a parent theory $A$ in a child theory $B$ for good. 

48 
The reason is that if some theory $C$ is based both on $B$ and (via a 

13814  49 
different path) on $A$, it is not defined what the simplification attribute 
12332  50 
of that theorem will be in $C$: it could be either. 
51 
\end{warn} 

11458  52 
*} 
9932  53 

11458  54 
subsection{*The {\tt\slshape simp} Method*} 
9932  55 

56 
text{*\index{*simp (method)bold} 

57 
The general format of the simplification method is 

58 
\begin{quote} 

59 
@{text simp} \textit{list of modifiers} 

60 
\end{quote} 

10795  61 
where the list of \emph{modifiers} fine tunes the behaviour and may 
11309  62 
be empty. Specific modifiers are discussed below. Most if not all of the 
63 
proofs seen so far could have been performed 

9932  64 
with @{text simp} instead of \isa{auto}, except that @{text simp} attacks 
10971  65 
only the first subgoal and may thus need to be repeated  use 
11428  66 
\methdx{simp_all} to simplify all subgoals. 
11458  67 
If nothing changes, @{text simp} fails. 
9932  68 
*} 
69 

11214  70 
subsection{*Adding and Deleting Simplification Rules*} 
9932  71 

72 
text{* 

11458  73 
\index{simplification rules!adding and deleting}% 
9932  74 
If a certain theorem is merely needed in a few proofs by simplification, 
75 
we do not need to make it a global simplification rule. Instead we can modify 

76 
the set of simplification rules used in a simplification step by adding rules 

77 
to it and/or deleting rules from it. The two modifiers for this are 

78 
\begin{quote} 

11458  79 
@{text"add:"} \textit{list of theorem names}\index{*add (modifier)}\\ 
80 
@{text"del:"} \textit{list of theorem names}\index{*del (modifier)} 

9932  81 
\end{quote} 
11458  82 
Or you can use a specific list of theorems and omit all others: 
9932  83 
\begin{quote} 
11458  84 
@{text"only:"} \textit{list of theorem names}\index{*only (modifier)} 
9932  85 
\end{quote} 
11309  86 
In this example, we invoke the simplifier, adding two distributive 
87 
laws: 

88 
\begin{quote} 

89 
\isacommand{apply}@{text"(simp add: mod_mult_distrib add_mult_distrib)"} 

90 
\end{quote} 

9932  91 
*} 
92 

11214  93 
subsection{*Assumptions*} 
9932  94 

95 
text{*\index{simplification!with/of assumptions} 

96 
By default, assumptions are part of the simplification process: they are used 

97 
as simplification rules and are simplified themselves. For example: 

98 
*} 

99 

12631  100 
lemma "\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \<rbrakk> \<Longrightarrow> ys = zs" 
101 
apply simp 

10171  102 
done 
9932  103 

104 
text{*\noindent 

105 
The second assumption simplifies to @{term"xs = []"}, which in turn 

106 
simplifies the first assumption to @{term"zs = ys"}, thus reducing the 

107 
conclusion to @{term"ys = ys"} and hence to @{term"True"}. 

108 

11458  109 
In some cases, using the assumptions can lead to nontermination: 
9932  110 
*} 
111 

12631  112 
lemma "\<forall>x. f x = g (f (g x)) \<Longrightarrow> f [] = f [] @ []" 
9932  113 

114 
txt{*\noindent 

11458  115 
An unmodified application of @{text"simp"} loops. The culprit is the 
116 
simplification rule @{term"f x = g (f (g x))"}, which is extracted from 

117 
the assumption. (Isabelle notices certain simple forms of 

118 
nontermination but not this one.) The problem can be circumvented by 

119 
telling the simplifier to ignore the assumptions: 

9932  120 
*} 
121 

12631  122 
apply(simp (no_asm)) 
10171  123 
done 
9932  124 

125 
text{*\noindent 

11458  126 
Three modifiers influence the treatment of assumptions: 
9932  127 
\begin{description} 
11458  128 
\item[@{text"(no_asm)"}]\index{*no_asm (modifier)} 
9932  129 
means that assumptions are completely ignored. 
11458  130 
\item[@{text"(no_asm_simp)"}]\index{*no_asm_simp (modifier)} 
9932  131 
means that the assumptions are not simplified but 
132 
are used in the simplification of the conclusion. 

11458  133 
\item[@{text"(no_asm_use)"}]\index{*no_asm_use (modifier)} 
9932  134 
means that the assumptions are simplified but are not 
135 
used in the simplification of each other or the conclusion. 

136 
\end{description} 

10795  137 
Both @{text"(no_asm_simp)"} and @{text"(no_asm_use)"} run forever on 
138 
the problematic subgoal above. 

11458  139 
Only one of the modifiers is allowed, and it must precede all 
11309  140 
other modifiers. 
13623  141 
%\begin{warn} 
142 
%Assumptions are simplified in a lefttoright fashion. If an 

143 
%assumption can help in simplifying one to the left of it, this may get 

144 
%overlooked. In such cases you have to rotate the assumptions explicitly: 

145 
%\isacommand{apply}@ {text"("}\methdx{rotate_tac}~$n$@ {text")"} 

146 
%causes a cyclic shift by $n$ positions from right to left, if $n$ is 

147 
%positive, and from left to right, if $n$ is negative. 

148 
%Beware that such rotations make proofs quite brittle. 

149 
%\end{warn} 

9932  150 
*} 
151 

11214  152 
subsection{*Rewriting with Definitions*} 
9932  153 

11215  154 
text{*\label{sec:SimpwithDefs}\index{simplification!with definitions} 
11458  155 
Constant definitions (\S\ref{sec:ConstDefinitions}) can be used as 
156 
simplification rules, but by default they are not: the simplifier does not 

157 
expand them automatically. Definitions are intended for introducing abstract 

12582
b85acd66f715
removed Misc/Translations (text covered by Documents.thy);
wenzelm
parents:
12533
diff
changeset

158 
concepts and not merely as abbreviations. Of course, we need to expand 
11458  159 
the definition initially, but once we have proved enough abstract properties 
160 
of the new constant, we can forget its original definition. This style makes 

161 
proofs more robust: if the definition has to be changed, 

162 
only the proofs of the abstract properties will be affected. 

163 

164 
For example, given *} 

9932  165 

10788  166 
constdefs xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" 
12631  167 
"xor A B \<equiv> (A \<and> \<not>B) \<or> (\<not>A \<and> B)" 
9932  168 

169 
text{*\noindent 

170 
we may want to prove 

171 
*} 

172 

12631  173 
lemma "xor A (\<not>A)" 
9932  174 

175 
txt{*\noindent 

11428  176 
Typically, we begin by unfolding some definitions: 
177 
\indexbold{definitions!unfolding} 

9932  178 
*} 
179 

12631  180 
apply(simp only: xor_def) 
9932  181 

182 
txt{*\noindent 

183 
In this particular case, the resulting goal 

10362  184 
@{subgoals[display,indent=0]} 
10171  185 
can be proved by simplification. Thus we could have proved the lemma outright by 
12631  186 
*}(*<*)oops lemma "xor A (\<not>A)"(*>*) 
10788  187 
apply(simp add: xor_def) 
10171  188 
(*<*)done(*>*) 
9932  189 
text{*\noindent 
190 
Of course we can also unfold definitions in the middle of a proof. 

191 

192 
\begin{warn} 

10971  193 
If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold 
194 
occurrences of $f$ with at least two arguments. This may be helpful for unfolding 

195 
$f$ selectively, but it may also get in the way. Defining 

196 
$f$~\isasymequiv~\isasymlambda$x\,y.\;t$ allows to unfold all occurrences of $f$. 

9932  197 
\end{warn} 
12473  198 

199 
There is also the special method \isa{unfold}\index{*unfold (method)bold} 

200 
which merely unfolds 

201 
one or several definitions, as in \isacommand{apply}\isa{(unfold xor_def)}. 

202 
This is can be useful in situations where \isa{simp} does too much. 

12533  203 
Warning: \isa{unfold} acts on all subgoals! 
9932  204 
*} 
205 

11214  206 
subsection{*Simplifying {\tt\slshape let}Expressions*} 
9932  207 

11458  208 
text{*\index{simplification!of \isa{let}expressions}\index{*let expressions}% 
209 
Proving a goal containing \isa{let}expressions almost invariably requires the 

210 
@{text"let"}con\structs to be expanded at some point. Since 

211 
@{text"let"}\ldots\isa{=}\ldots@{text"in"}{\ldots} is just syntactic sugar for 

212 
the predefined constant @{term"Let"}, expanding @{text"let"}constructs 

213 
means rewriting with \tdx{Let_def}: *} 

9932  214 

12631  215 
lemma "(let xs = [] in xs@ys@xs) = ys" 
216 
apply(simp add: Let_def) 

10171  217 
done 
9932  218 

219 
text{* 

220 
If, in a particular context, there is no danger of a combinatorial explosion 

11458  221 
of nested @{text"let"}s, you could even simplify with @{thm[source]Let_def} by 
9932  222 
default: 
223 
*} 

224 
declare Let_def [simp] 

225 

11458  226 
subsection{*Conditional Simplification Rules*} 
9932  227 

228 
text{* 

11458  229 
\index{conditional simplification rules}% 
9932  230 
So far all examples of rewrite rules were equations. The simplifier also 
231 
accepts \emph{conditional} equations, for example 

232 
*} 

233 

12631  234 
lemma hd_Cons_tl[simp]: "xs \<noteq> [] \<Longrightarrow> hd xs # tl xs = xs" 
235 
apply(case_tac xs, simp, simp) 

10171  236 
done 
9932  237 

238 
text{*\noindent 

239 
Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a 

240 
sequence of methods. Assuming that the simplification rule 

241 
@{term"(rev xs = []) = (xs = [])"} 

242 
is present as well, 

10795  243 
the lemma below is proved by plain simplification: 
9932  244 
*} 
245 

12631  246 
lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs" 
9932  247 
(*<*) 
12631  248 
by(simp) 
9932  249 
(*>*) 
250 
text{*\noindent 

10795  251 
The conditional equation @{thm[source]hd_Cons_tl} above 
9932  252 
can simplify @{term"hd(rev xs) # tl(rev xs)"} to @{term"rev xs"} 
253 
because the corresponding precondition @{term"rev xs ~= []"} 

254 
simplifies to @{term"xs ~= []"}, which is exactly the local 

255 
assumption of the subgoal. 

256 
*} 

257 

258 

11214  259 
subsection{*Automatic Case Splits*} 
9932  260 

11458  261 
text{*\label{sec:AutoCaseSplits}\indexbold{case splits}% 
262 
Goals containing @{text"if"}expressions\index{*if expressions!splitting of} 

263 
are usually proved by case 

264 
distinction on the boolean condition. Here is an example: 

9932  265 
*} 
266 

12631  267 
lemma "\<forall>xs. if xs = [] then rev xs = [] else rev xs \<noteq> []" 
9932  268 

269 
txt{*\noindent 

11458  270 
The goal can be split by a special method, \methdx{split}: 
9932  271 
*} 
272 

10654  273 
apply(split split_if) 
9932  274 

10362  275 
txt{*\noindent 
276 
@{subgoals[display,indent=0]} 

11428  277 
where \tdx{split_if} is a theorem that expresses splitting of 
10654  278 
@{text"if"}s. Because 
11458  279 
splitting the @{text"if"}s is usually the right proof strategy, the 
280 
simplifier does it automatically. Try \isacommand{apply}@{text"(simp)"} 

9932  281 
on the initial goal above. 
282 

11428  283 
This splitting idea generalizes from @{text"if"} to \sdx{case}. 
11458  284 
Let us simplify a case analysis over lists:\index{*list.split (theorem)} 
10654  285 
*}(*<*)by simp(*>*) 
12631  286 
lemma "(case xs of [] \<Rightarrow> zs  y#ys \<Rightarrow> y#(ys@zs)) = xs@zs" 
287 
apply(split list.split) 

11309  288 

10362  289 
txt{* 
290 
@{subgoals[display,indent=0]} 

11458  291 
The simplifier does not split 
292 
@{text"case"}expressions, as it does @{text"if"}expressions, 

293 
because with recursive datatypes it could lead to nontermination. 

294 
Instead, the simplifier has a modifier 

11494  295 
@{text split}\index{*split (modifier)} 
11458  296 
for adding splitting rules explicitly. The 
297 
lemma above can be proved in one step by 

9932  298 
*} 
12631  299 
(*<*)oops 
300 
lemma "(case xs of [] \<Rightarrow> zs  y#ys \<Rightarrow> y#(ys@zs)) = xs@zs" 

9932  301 
(*>*) 
12631  302 
apply(simp split: list.split) 
10171  303 
(*<*)done(*>*) 
10654  304 
text{*\noindent 
305 
whereas \isacommand{apply}@{text"(simp)"} alone will not succeed. 

9932  306 

11458  307 
Every datatype $t$ comes with a theorem 
9932  308 
$t$@{text".split"} which can be declared to be a \bfindex{split rule} either 
11458  309 
locally as above, or by giving it the \attrdx{split} attribute globally: 
9932  310 
*} 
311 

312 
declare list.split [split] 

313 

314 
text{*\noindent 

315 
The @{text"split"} attribute can be removed with the @{text"del"} modifier, 

316 
either locally 

317 
*} 

318 
(*<*) 

12631  319 
lemma "dummy=dummy" 
9932  320 
(*>*) 
12631  321 
apply(simp split del: split_if) 
9932  322 
(*<*) 
12631  323 
oops 
9932  324 
(*>*) 
325 
text{*\noindent 

326 
or globally: 

327 
*} 

328 
declare list.split [split del] 

329 

330 
text{* 

11458  331 
Polished proofs typically perform splitting within @{text simp} rather than 
332 
invoking the @{text split} method. However, if a goal contains 

19792  333 
several @{text "if"} and @{text case} expressions, 
11458  334 
the @{text split} method can be 
10654  335 
helpful in selectively exploring the effects of splitting. 
336 

11458  337 
The split rules shown above are intended to affect only the subgoal's 
338 
conclusion. If you want to split an @{text"if"} or @{text"case"}expression 

339 
in the assumptions, you have to apply \tdx{split_if_asm} or 

340 
$t$@{text".split_asm"}: *} 

9932  341 

10654  342 
lemma "if xs = [] then ys \<noteq> [] else ys = [] \<Longrightarrow> xs @ ys \<noteq> []" 
343 
apply(split split_if_asm) 

9932  344 

10362  345 
txt{*\noindent 
11458  346 
Unlike splitting the conclusion, this step creates two 
347 
separate subgoals, which here can be solved by @{text"simp_all"}: 

10362  348 
@{subgoals[display,indent=0]} 
9932  349 
If you need to split both in the assumptions and the conclusion, 
350 
use $t$@{text".splits"} which subsumes $t$@{text".split"} and 

351 
$t$@{text".split_asm"}. Analogously, there is @{thm[source]if_splits}. 

352 

353 
\begin{warn} 

11458  354 
The simplifier merely simplifies the condition of an 
355 
\isa{if}\index{*if expressions!simplification of} but not the 

9932  356 
\isa{then} or \isa{else} parts. The latter are simplified only after the 
357 
condition reduces to \isa{True} or \isa{False}, or after splitting. The 

11428  358 
same is true for \sdx{case}expressions: only the selector is 
9932  359 
simplified at first, until either the expression reduces to one of the 
360 
cases or it is split. 

11458  361 
\end{warn} 
9932  362 
*} 
10362  363 
(*<*) 
364 
by(simp_all) 

365 
(*>*) 

9932  366 

11214  367 
subsection{*Tracing*} 
9932  368 
text{*\indexbold{tracing the simplifier} 
369 
Using the simplifier effectively may take a bit of experimentation. Set the 

16523  370 
Proof General flag \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$ \pgmenu{Trace Simplifier} to get a better idea of what is going on: 
9932  371 
*} 
372 

12631  373 
lemma "rev [a] = []" 
374 
apply(simp) 

9932  375 
(*<*)oops(*>*) 
376 

377 
text{*\noindent 

16523  378 
produces the following trace in Proof General's \pgmenu{Trace} buffer: 
9932  379 

380 
\begin{ttbox}\makeatother 

16518  381 
[1]Applying instance of rewrite rule "List.rev.simps_2": 
16359  382 
rev (?x1 # ?xs1) \(\equiv\) rev ?xs1 @ [?x1] 
383 

16518  384 
[1]Rewriting: 
16359  385 
rev [a] \(\equiv\) rev [] @ [a] 
386 

16518  387 
[1]Applying instance of rewrite rule "List.rev.simps_1": 
16359  388 
rev [] \(\equiv\) [] 
389 

16518  390 
[1]Rewriting: 
16359  391 
rev [] \(\equiv\) [] 
392 

16518  393 
[1]Applying instance of rewrite rule "List.op @.append_Nil": 
16359  394 
[] @ ?y \(\equiv\) ?y 
395 

16518  396 
[1]Rewriting: 
16359  397 
[] @ [a] \(\equiv\) [a] 
398 

16518  399 
[1]Applying instance of rewrite rule 
16359  400 
?x2 # ?t1 = ?t1 \(\equiv\) False 
401 

16518  402 
[1]Rewriting: 
16359  403 
[a] = [] \(\equiv\) False 
9932  404 
\end{ttbox} 
16359  405 
The trace lists each rule being applied, both in its general form and 
406 
the instance being used. The \texttt{[}$i$\texttt{]} in front (where 

16518  407 
above $i$ is always \texttt{1}) indicates that we are inside the $i$th 
408 
invocation of the simplifier. Each attempt to apply a 

16359  409 
conditional rule shows the rule followed by the trace of the 
410 
(recursive!) simplification of the conditions, the latter prefixed by 

411 
\texttt{[}$i+1$\texttt{]} instead of \texttt{[}$i$\texttt{]}. 

412 
Another source of recursive invocations of the simplifier are 

413 
proofs of arithmetic formulae. 

11309  414 

16359  415 
Many other hints about the simplifier's actions may appear. 
9932  416 

16359  417 
In more complicated cases, the trace can be very lengthy. Thus it is 
16523  418 
advisable to reset the \pgmenu{Trace Simplifier} flag after having 
16359  419 
obtained the desired trace. *} 
9932  420 

16544  421 
subsection{*Finding Theorems\label{sec:find}*} 
16518  422 

16523  423 
text{*\indexbold{finding theorems}\indexbold{searching theorems} 
16560  424 
Isabelle's large database of proved theorems 
425 
offers a powerful search engine. Its chief limitation is 

16518  426 
its restriction to the theories currently loaded. 
427 

428 
\begin{pgnote} 

16523  429 
The search engine is started by clicking on Proof General's \pgmenu{Find} icon. 
16518  430 
You specify your search textually in the input buffer at the bottom 
431 
of the window. 

432 
\end{pgnote} 

433 

16560  434 
The simplest form of search finds theorems containing specified 
435 
patterns. A pattern can be any term (even 

436 
a single identifier). It may contain ``\texttt{\_}'', a wildcard standing 

437 
for any term. Here are some 

16518  438 
examples: 
439 
\begin{ttbox} 

440 
length 

441 
"_ # _ = _ # _" 

442 
"_ + _" 

443 
"_ * (_  (_::nat))" 

444 
\end{ttbox} 

16560  445 
Specifying types, as shown in the last example, 
446 
constrains searches involving overloaded operators. 

16518  447 

448 
\begin{warn} 

449 
Always use ``\texttt{\_}'' rather than variable names: searching for 

450 
\texttt{"x + y"} will usually not find any matching theorems 

16560  451 
because they would need to contain \texttt{x} and~\texttt{y} literally. 
452 
When searching for infix operators, do not just type in the symbol, 

453 
such as~\texttt{+}, but a proper term such as \texttt{"_ + _"}. 

454 
This remark applies to more complicated syntaxes, too. 

16518  455 
\end{warn} 
456 

16560  457 
If you are looking for rewrite rules (possibly conditional) that could 
458 
simplify some term, prefix the pattern with \texttt{simp:}. 

16518  459 
\begin{ttbox} 
460 
simp: "_ * (_ + _)" 

461 
\end{ttbox} 

16560  462 
This finds \emph{all} equationsnot just those with a \isa{simp} attributewhose conclusion has the form 
16518  463 
@{text[display]"_ * (_ + _) = \<dots>"} 
16560  464 
It only finds equations that can simplify the given pattern 
465 
at the root, not somewhere inside: for example, equations of the form 

466 
@{text"_ + _ = \<dots>"} do not match. 

16518  467 

16560  468 
You may also search for theorems by nameyou merely 
469 
need to specify a substring. For example, you could search for all 

16518  470 
commutativity theorems like this: 
471 
\begin{ttbox} 

472 
name: comm 

473 
\end{ttbox} 

474 
This retrieves all theorems whose name contains \texttt{comm}. 

475 

16560  476 
Search criteria can also be negated by prefixing them with ``\texttt{}''. 
477 
For example, 

16518  478 
\begin{ttbox} 
16523  479 
name: List 
16518  480 
\end{ttbox} 
16560  481 
finds theorems whose name does not contain \texttt{List}. You can use this 
482 
to exclude particular theories from the search: the long name of 

16518  483 
a theorem contains the name of the theory it comes from. 
484 

16560  485 
Finallly, different search criteria can be combined arbitrarily. 
20143  486 
The effect is conjuctive: Find returns the theorems that satisfy all of 
16560  487 
the criteria. For example, 
16518  488 
\begin{ttbox} 
489 
"_ + _" "_  _" simp: "_ * (_ + _)" name: assoc 

490 
\end{ttbox} 

16560  491 
looks for theorems containing plus but not minus, and which do not simplify 
492 
\mbox{@{text"_ * (_ + _)"}} at the root, and whose name contains \texttt{assoc}. 

16518  493 

16544  494 
Further search criteria are explained in \S\ref{sec:find2}. 
16523  495 

496 
\begin{pgnote} 

497 
Proof General keeps a history of all your search expressions. 

498 
If you click on \pgmenu{Find}, you can use the arrow keys to scroll 

499 
through previous searches and just modify them. This saves you having 

500 
to type in lengthy expressions again and again. 

501 
\end{pgnote} 

16518  502 
*} 
9932  503 
(*<*) 
9922  504 
end 
9932  505 
(*>*) 