diff -r 84aef87b348a -r ffa5c4ec9611 ProgTutorial/Tactical.thy --- 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 \ \ \"} 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 \ Q \ Q \ 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 \ Q \ Q \ 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