CookBook/Tactical.thy
changeset 184 c7f04a008c9c
parent 178 fb8f22dd8ad0
child 186 371e4375c994
--- 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) *}