Mercurial Mercurial > hg > regexp / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
a few bits on the journal paper
authorurbanc
Thu, 25 Aug 2011 19:33:41 +0000
changeset 217 05da74214979
parent 216 36fe0806b6f0
child 218 28e98ede8599
a few bits on the journal paper
Journal/Paper.thy file | annotate | diff | comparison | revisions 
--- 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