# HG changeset patch # User boehmes # Date 1235652365 -3600 # Node ID d3fcc1a0272c03e8b08e717cf7aaf0800770e9c1 # Parent 253ea99c144195fb8ff8712ac99b58f779d05f5b Corrected small mistake. 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