
diff -r 12e9aa68d5db -r 4190df6f4488 Matcher.thy
--- a/Matcher.thy	Mon Dec 26 08:21:00 2011 +0000
+++ b/Matcher.thy	Tue Jan 24 00:20:09 2012 +0000
@@ -171,6 +171,17 @@
 
 section {* Examples *}
 
+definition 
+  "CHRA \<equiv> CHAR (CHR ''a'')"
+
+definition 
+  "ALT1 \<equiv> ALT CHRA EMPTY"
+
+definition 
+  "SEQ3 \<equiv> SEQ (SEQ ALT1 ALT1) ALT1"
+
+value "matcher SEQ3 ''aaa''"
+
 value "matcher NULL []"
 value "matcher (CHAR (CHR ''a'')) [CHR ''a'']"
 value "matcher (CHAR a) [a,a]"




