--- a/ProgTutorial/Tactical.thy Wed Aug 20 14:42:14 2014 +0100
+++ b/ProgTutorial/Tactical.thy Wed Oct 15 23:12:54 2014 +0100
@@ -18,13 +18,13 @@
Donald E.~Knuth, from an interview in Dr.~Dobb's Journal, 1996.
\end{flushright}
- One of the main reason for descending to the ML-level of Isabelle is to be
- able to implement automatic proof procedures. Such proof procedures can
+ One of the main reason for descending to the ML-level of Isabelle is to
+ implement automatic proof procedures. Such proof procedures can
considerably lessen the burden of manual reasoning. They are centred around
the idea of refining a goal state using tactics. This is similar to the
\isacommand{apply}-style reasoning at the user-level, where goals are
modified in a sequence of proof steps until all of them are discharged.
- In this chapter we will explain simple tactics and how to combine them using
+ In this chapter we explain how to implement simple tactics and how to combine them using
tactic combinators. We also describe the simplifier, simprocs and conversions.
*}
@@ -113,7 +113,7 @@
text {*
By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} you can call from the
user-level of Isabelle the tactic @{ML foo_tac} or
- any other function that returns a tactic. There are some goal transformation
+ any other function that returns a tactic. There are some goal transformations
that are performed by @{text "tactic"}. They can be avoided by using
@{text "raw_tactic"} instead.
@@ -138,7 +138,7 @@
one such combinator---a ``primed'' version exists.) With @{ML foo_tac'} you
can give the number for the subgoal explicitly when the tactic is called. So
in the next proof you can first discharge the second subgoal, and
- subsequently the first.
+ then the first.
*}
lemma
@@ -152,8 +152,8 @@
This kind of addressing is more difficult to achieve when the goal is
hard-coded inside the tactic.
- The tactics @{ML foo_tac} and @{ML foo_tac'} are very specific for analysing
- goals being only of the form @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not of
+ The tactics @{ML foo_tac} and @{ML foo_tac'} are specific
+ to goals of the form @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not of
this form, then these tactics return the error message:\footnote{To be
precise, tactics do not produce this error message; the message originates from the
\isacommand{apply} wrapper that calls the tactic.}
@@ -173,8 +173,8 @@
text {*
By convention, if a tactic fails, then it should return the empty sequence.
- Therefore, if you write your own tactics, they should not raise exceptions
- willy-nilly; only in very grave failure situations should a tactic raise the
+ Therefore, your own tactics should not raise exceptions
+ willy-nilly; only in very grave failure situations should a tactic raise the
exception @{text THM}.
The simplest tactics are @{ML_ind no_tac in Tactical} and