diff -r 253ea99c1441 -r d3fcc1a0272c CookBook/Tactical.thy --- a/CookBook/Tactical.thy Thu Feb 26 12:16:24 2009 +0000 +++ b/CookBook/Tactical.thy Thu Feb 26 13:46:05 2009 +0100 @@ -1323,7 +1323,7 @@ text {* Conversions are a thin layer on top of Isabelle's inference kernel, and - can be viewed be as a controllable, bare-bone version of Isabelle's simplifier. + can be viewed as a controllable, bare-bone version of Isabelle's simplifier. One difference between conversions and the simplifier is that the former act on @{ML_type cterm}s while the latter acts on @{ML_type thm}s. However, we will also show in this section how conversions can be applied