# HG changeset patch
# User urbanc
# Date 1314300821 0
# Node ID 05da74214979340f14b7c43b3b3846ac4e9fa668
# Parent  36fe0806b6f02fc276f75fc366d57b79488e8a0c
a few bits on the journal paper

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.