Matcher.thy
changeset 262 4190df6f4488
parent 155 d8d1e1f53d6e
--- 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]"