
diff -r 8def50824320 -r f4c9dd7bcb28 ProgTutorial/Tactical.thy
--- 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




