diff -r 0634d42bb69f -r 17b1512f51af ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Tue Mar 24 18:06:20 2009 +0100 +++ b/ProgTutorial/Tactical.thy Wed Mar 25 15:09:04 2009 +0100 @@ -515,7 +515,8 @@ theorem in the first. @{ML_response_fake [display,gray] - "[@{thm impI}, @{thm disjI2}] RL [@{thm conjI}, @{thm disjI1}]" +"map (no_vars @{context}) + ([@{thm impI}, @{thm disjI2}] RL [@{thm conjI}, @{thm disjI1}])" "[\P \ Q; Qa\ \ (P \ Q) \ Qa, \Q; Qa\ \ (P \ Q) \ Qa, (P \ Q) \ (P \ Q) \ Qa, @@ -1067,7 +1068,7 @@ text {* If the simplifier cannot make any progress, then it leaves the goal unchanged, - i.e.~does not raise any error message. That means if you use it to unfold a + i.e., does not raise any error message. That means if you use it to unfold a definition for a constant and this constant is not present in the goal state, you can still safely apply the simplifier. @@ -1117,11 +1118,11 @@ \end{readmore} \begin{readmore} - FIXME: Find the right place Discrimination nets are implemented + FIXME: Find the right place: Discrimination nets are implemented in @{ML_file "Pure/net.ML"}. \end{readmore} - The most common combinators to modify simpsets are + The most common combinators to modify simpsets are: \begin{isabelle} \begin{tabular}{ll} @@ -1170,7 +1171,7 @@ text {* To see how they work, consider the function in Figure~\ref{fig:printss}, which prints out some parts of a simpset. If you use it to print out the components of the - empty simpset, i.e.~ @{ML empty_ss} + empty simpset, i.e., @{ML empty_ss} @{ML_response_fake [display,gray] "print_ss @{context} empty_ss" @@ -1351,7 +1352,7 @@ it would be desirable to add also the lemma @{thm [source] perm_compose} to the simplifier for pushing permutations over other permutations. Unfortunately, the right-hand side of this lemma is again an instance of the left-hand side - and so causes an infinite loop. The seems to be no easy way to reformulate + and so causes an infinite loop. There seems to be no easy way to reformulate this rule and so one ends up with clunky proofs like: *} @@ -1417,7 +1418,7 @@ end*} text {* - For all three phases we have to build simpsets addig specific lemmas. As is sufficient + For all three phases we have to build simpsets adding specific lemmas. As is sufficient for our purposes here, we can add these lemma to @{ML HOL_basic_ss} in order to obtain the desired results. Now we can solve the following lemma *} @@ -1430,8 +1431,8 @@ text {* - in one step. This tactic can deal with most instances of normalising permutations; - in order to solve all cases we have to deal with corner-cases such as the + in one step. This tactic can deal with most instances of normalising permutations. + In order to solve all cases we have to deal with corner-cases such as the lemma being an exact instance of the permutation composition lemma. This can often be done easier by implementing a simproc or a conversion. Both will be explained in the next two chapters.