--- a/progs/Matcher2.thy	Fri Apr 18 21:05:07 2014 +0100
+++ b/progs/Matcher2.thy	Thu Aug 21 15:10:53 2014 +0100
@@ -152,6 +152,10 @@
 | "L (NTIMES r n) = (L r) \<up> n"
 | "L (NMTIMES r n m) = (\<Union>i\<in> {n..n+m} . ((L r) \<up> i))" 
 
+lemma "L (NOT NULL) = UNIV"
+apply(simp)
+done
+
 
 section {* The Matcher *}