aboutsummaryrefslogtreecommitdiffhomepage
path: root/etc/isar/NamesInStrings.thy
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2004-06-16 16:05:45 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2004-06-16 16:05:45 +0000
commit27e42b688f8bc872a0d6c18f8a91c2b6e2320aa6 (patch)
treec6a82a8777e5badc3a5691a7246527f410569db4 /etc/isar/NamesInStrings.thy
parentc7b48379944d4aca3f86160495b23cb8b2940d91 (diff)
*** empty log message ***
Diffstat (limited to 'etc/isar/NamesInStrings.thy')
-rw-r--r--etc/isar/NamesInStrings.thy3
1 files changed, 2 insertions, 1 deletions
diff --git a/etc/isar/NamesInStrings.thy b/etc/isar/NamesInStrings.thy
index b8afc467..cf650298 100644
--- a/etc/isar/NamesInStrings.thy
+++ b/etc/isar/NamesInStrings.thy
@@ -9,7 +9,8 @@ lemma "foo-wiggle-bar": "B --> B" by auto
theorem "x b": "B --> B" by auto
(* NB: various other regexps and settings based on them are sensitive
- to grouping in isar-name-regexp. *)
+ to grouping in isar-name-regexp: should check function menu, imenu,
+ as well as undo behaviour. *)
end