--- a/ProgTutorial/Tactical.thy Tue Apr 07 23:59:39 2009 +0100
+++ b/ProgTutorial/Tactical.thy Wed Apr 08 09:22:07 2009 +0200
@@ -70,7 +70,7 @@
Note that in the code above we use antiquotations for referencing the theorems. Many theorems
also have ML-bindings with the same name. Therefore, we could also just have
- written @{ML "etac disjE 1"}, or in case where there are no ML-binding obtain
+ written @{ML "etac disjE 1"}, or in case where there is no ML-binding obtain
the theorem dynamically using the function @{ML thm}; for example
\mbox{@{ML "etac (thm \"disjE\") 1"}}. Both ways however are considered bad style!
The reason
@@ -314,7 +314,7 @@
a ``protector'' wrapped around it (the wrapper is the outermost constant @{text
"Const (\"prop\", bool \<Rightarrow> bool)"}; however this constant
is invisible in the figure). This wrapper prevents that premises of @{text C} are
- mis-interpreted as open subgoals. While tactics can operate on the subgoals
+ misinterpreted as open subgoals. While tactics can operate on the subgoals
(the @{text "A\<^isub>i"} above), they are expected to leave the conclusion
@{term C} intact, with the exception of possibly instantiating schematic
variables. If you use the predefined tactics, which we describe in the next
@@ -1020,7 +1020,7 @@
powerful simplifier. The power of simplifier is a strength and a weakness at
the same time, because you can easily make the simplifier to run into a loop and its
behaviour can be difficult to predict. There is also a multitude
- of options that you can configurate to control the behaviour of the simplifier.
+ of options that you can configure to control the behaviour of the simplifier.
We describe some of them in this and the next section.
There are the following five main tactics behind
@@ -1038,7 +1038,7 @@
\end{center}
\end{isabelle}
- All of the tactics take a simpset and an interger as argument (the latter as usual
+ All of the tactics take a simpset and an integer as argument (the latter as usual
to specify the goal to be analysed). So the proof
*}
@@ -1067,7 +1067,7 @@
simpset is more complex than just a simple collection of theorems used as
simplification rules. One reason for the complexity is that the simplifier
must be able to rewrite inside terms and should also be able to rewrite
- according to rules that have precoditions.
+ according to rules that have preconditions.
The rewriting inside terms requires congruence rules, which
@@ -1082,7 +1082,7 @@
with @{text "constr"} being a term-constructor, like @{const "If"} or @{const "Let"}.
Every simpset contains only
- one concruence rule for each term-constructor, which however can be
+ one congruence rule for each term-constructor, which however can be
overwritten. The user can declare lemmas to be congruence rules using the
attribute @{text "[cong]"}. In HOL, the user usually states these lemmas as
equations, which are then internally transformed into meta-equations.
@@ -1095,7 +1095,7 @@
simprocs, which can produce rewrite rules on demand (see next
section). Another component are split-rules, which can simplify for example
the ``then'' and ``else'' branches of if-statements under the corresponding
- precoditions.
+ preconditions.
\begin{readmore}
@@ -1149,7 +1149,7 @@
\end{minipage}
\caption{The function @{ML MetaSimplifier.dest_ss} returns a record containing
all printable information stored in a simpset. We are here only interested in the
- simplifcation rules, congruence rules and simprocs.\label{fig:printss}}
+ simplification rules, congruence rules and simprocs.\label{fig:printss}}
\end{figure} *}
text {*
@@ -1231,7 +1231,7 @@
This behaviour is not because of simplification rules, but how the subgoaler, solver
and looper are set up in @{ML HOL_basic_ss}.
- The simpset @{ML HOL_ss} is an extention of @{ML HOL_basic_ss} containing
+ The simpset @{ML HOL_ss} is an extension of @{ML HOL_basic_ss} containing
already many useful simplification and congruence rules for the logical
connectives in HOL.
@@ -1394,9 +1394,9 @@
of the left-hand side. In a sense it freezes all redexes of permutation compositions
after one step. In this way, we can split simplification of permutations
into three phases without the user noticing anything about the auxiliary
- contant. We first freeze any instance of permutation compositions in the term using
+ constant. We first freeze any instance of permutation compositions in the term using
lemma @{thm [source] "perm_aux_expand"} (Line 9);
- then simplifiy all other permutations including pushing permutations over
+ then simplify all other permutations including pushing permutations over
other permutations by rule @{thm [source] perm_compose_aux} (Line 10); and
finally ``unfreeze'' all instances of permutation compositions by unfolding
the definition of the auxiliary constant.
@@ -1560,7 +1560,7 @@
Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}).
The function also takes a list of patterns that can trigger the simproc.
Now the simproc is set up and can be explicitly added using
- @{ML addsimprocs} to a simpset whenerver
+ @{ML addsimprocs} to a simpset whenever
needed.
Simprocs are applied from inside to outside and from left to right. You can
@@ -1686,7 +1686,7 @@
The advantage of @{ML get_thm_alt} is that it leaves very little room for
something to go wrong; in contrast it is much more difficult to predict
what happens with @{ML arith_tac in Arith_Data}, especially in more complicated
- circumstances. The disatvantage of @{ML get_thm_alt} is to find a simpset
+ circumstances. The disadvantage of @{ML get_thm_alt} is to find a simpset
that is sufficiently powerful to solve every instance of the lemmas
we like to prove. This requires careful tuning, but is often necessary in
``production code''.\footnote{It would be of great help if there is another