From c7b48379944d4aca3f86160495b23cb8b2940d91 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 16 Jun 2004 16:05:22 +0000
Subject: New files.

---
 etc/isar/NamesInStrings.thy | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 etc/isar/NamesInStrings.thy

diff --git a/etc/isar/NamesInStrings.thy b/etc/isar/NamesInStrings.thy
new file mode 100644
index 00000000..b8afc467
--- /dev/null
+++ b/etc/isar/NamesInStrings.thy
@@ -0,0 +1,33 @@
+theory "a b" = Main:
+
+lemma foo: "B --> B" by auto
+
+lemma "foo bar": "B --> B" by auto
+
+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. *)
+
+end
+
+
+(*
+
+I noticed the following minor problem with Isabelle and 
+ProofGeneral:
+
+
+>>   theory "a" = Main:
+>>   Proof General -> Use -> Retract:
+>>   *** Outer syntax error: end of input expected,
+>>   *** but identifier "a" was found
+
+Regards,
+Tjark
+
+*)
+
+
-- 
cgit v1.2.3