149 | "L (NOT r) = UNIV - (L r)"

   149 | "L (NOT r) = UNIV - (L r)"

   150 | "L (PLUS r) = (L r) ;; ((L r)\<star>)"

   150 | "L (PLUS r) = (L r) ;; ((L r)\<star>)"

   151 | "L (OPT r) = (L r) \<union> {[]}"

   151 | "L (OPT r) = (L r) \<union> {[]}"

   152 | "L (NTIMES r n) = (L r) \<up> n"

   152 | "L (NTIMES r n) = (L r) \<up> n"

   153 | "L (NMTIMES r n m) = (\<Union>i\<in> {n..n+m} . ((L r) \<up> i))" 

   153 | "L (NMTIMES r n m) = (\<Union>i\<in> {n..n+m} . ((L r) \<up> i))" 

   154 

   158 

   155 

   159 

   156 section {* The Matcher *}

   160 section {* The Matcher *}

   157 

   161 

   158 fun

   162 fun