diff -r d3fe0597080a -r 5fed809d0fc1 Matcher.thy
--- a/Matcher.thy	Mon Feb 14 09:38:18 2011 +0000
+++ b/Matcher.thy	Mon Feb 14 11:12:01 2011 +0000
@@ -38,6 +38,14 @@
 | STAR rexp
 
 
+definition
+  "DERIV s A \<equiv> {s'. s @ s' \<in> A}"
+
+definition
+  "delta A = (if [] \<in> A then {[]} else {})"
+
+
+
 section {* Semantics of Regular Expressions *}
  
 fun