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 \ CHAR (CHR ''a'')" + +definition + "ALT1 \ ALT CHRA EMPTY" + +definition + "SEQ3 \ 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]"