
diff -r 36fe0806b6f0 -r 05da74214979 Journal/Paper.thy
--- a/Journal/Paper.thy	Thu Aug 25 06:19:42 2011 +0000
+++ b/Journal/Paper.thy	Thu Aug 25 19:33:41 2011 +0000
@@ -82,6 +82,7 @@
   pderivs_lang ("pdersl") and
   UNIV1 ("UNIV\<^isup>+") and
   Deriv_lang ("Dersl") and
+  Derivss ("Derss") and
   deriv ("der") and
   derivs ("ders") and
   pderiv ("pder") and
@@ -373,7 +374,8 @@
   define a regular language as one for which there exists \emph{a} finite
   automaton that recognises all its strings (see Definition~\ref{baddef}), then we
   need a lemma which ensures that another equivalent one can be found
-  satisfying the side-condition. Unfortunately, such `little' and `obvious'
+  satisfying the side-condition, and also need to make sure our operations on
+  automata preserve them. Unfortunately, such `little' and `obvious'
   lemmas make a formalisation of automata theory a hair-pulling experience.
 
 




