
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) *}




