Mercurial Mercurial > hg > regexp / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Journal/Paper.thy
changeset 217 05da74214979
parent 203 5d724fe0e096
child 218 28e98ede8599 
--- 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.
regexp