diff -r 8bb4eaa2ec92 -r c7f04a008c9c CookBook/Tactical.thy --- a/CookBook/Tactical.thy Tue Mar 17 17:32:12 2009 +0100 +++ b/CookBook/Tactical.thy Wed Mar 18 03:03:51 2009 +0100 @@ -2068,7 +2068,10 @@ *} - +text {* + (FIXME: check whether @{ML Pattern.match_rew} and @{ML Pattern.rewrite_term} + are of any use/efficient) +*} section {* Structured Proofs (TBD) *}