--- a/Journal/JAR-response	Wed Jul 10 17:47:30 2013 +0100
+++ b/Journal/JAR-response	Wed Jul 10 17:59:00 2013 +0100
@@ -150,8 +150,8 @@
 
 We disagree in that we should not take the opportunity of using 
 regular expressions when they lead to simpler formalisations
-in regular language theory. We have already found that many structural 
-inductions that only regular expressions afford are good learning 
+in regular language theory. We have already found as one "application"
+that many structural inductions over regular expressions are good learning 
 tools for students in order to come to grips with formal reasoning. 
 
 
@@ -163,7 +163,7 @@
 no proof, for which he refers to Arden (1960). Unfortunately, we do not have 
 access to this book and guess that this applies to many contemporary readers.
 Our reference to Sakarovitch is motivated by the fact that he gives 
-explicitly a proof (XXX CHECK). 
+explicitly a proof. 
 
 > - I am puzzled by the one-character transition relation between
 >   equivalence classes (p. 6). The $X_i$ correspond to the states of
@@ -327,7 +327,7 @@
 
 In our opinion, Coquand and Siles' development strongly justifies our 
 comment about formalisation of Brzozowski's argument being painful.
-If you like to add this as a reference in the paper, we are happy
+If you like to have this reference added in the paper, we are happy
 to do so. 
 
 > - Section 6, p20, previous to last paragraph: you say that the
@@ -336,7 +336,7 @@
 >   non-deterministic automaton, since it can be avoided using
 >   Antimirov's construction of a DFA (as you do).
 
-We feel that our sequence adequately represents procedure
+We feel that our sequence adequately represents the procedure
 that is used by informed outsiders and that is usually 
 taught to students. Antimirov's construction using partial
 derivatives is unfortunately not widely known, which we hope
@@ -353,16 +353,16 @@
 >   some of the arguments you are using. Is it possible in Isabelle/HOL
 >   to track what are the uses of classical logic that you use? 
 
-In theory there is a way to track all classical uses in Isabelle,
+In theory there is a way to track all classical uses in Isabelle/HOL,
 but this can be practically unfeasible, since proof terms can be 
 gigantic (therefore the Isabelle/HOL follows the LCF approach 
 where only theorems need to be recorded for correctness). Having 
-said that there is one obvious place in our proof where we used 
+said that, there is one obvious place in our proof where we used 
 a "classical" shortcut by using + for generating a single regular 
 expression from a finite set of expressions. This would need better 
 "explanation" in a constructive proof. There are no other inherent
-classical shortcuts in the proof. But as said before opening we
-think opening this can-of-worms is beside the focus of the paper.
+classical shortcuts in the proof. But as said before, we think opening 
+this can-of-worms is beside the focus of the paper.
 
 
 >  In particular, I am worried about the last sentence on page 24: how do
@@ -386,8 +386,8 @@
 >   equivalences classes of your Myhill-Nerode relation?  
 
 We have attempted to be very careful with our comments about the
-formalisation sizes from other works. Our intention is only to draw
-attention to the somewhat surprising point, namely that formalisation
+formalisation sizes from other works. Our point is to draw
+attention to the somewhat surprising fact, namely that formalisation
 using automata (either out of choice or being forced) led to 
 formalisations where the people in question had to fight their
 theorem prover. On the other hand, our formalisation could rely
@@ -407,8 +407,8 @@
 >   to computational algebra in COQ. ITP 2012. It does not seem that
 >   there is a particular problem with the use of matrices. 
 
-We relied completely on the comment by (expert formaliser in Coq) Braibant 
-from his thesis which explicitly states 
+We relied completely on the comment by (we assume expert formaliser in Coq) 
+Braibant from his thesis which explicitly states: 
 
   | Note that while they [Wu, Zhang, Urban] justify their work by the fact  
   | that formalising automata ``can be a real hassle in HOL-based provers'', 
@@ -444,14 +444,15 @@
 > re-read with more care.
 
 We have improved the paper. Please let us know if we
-overlooked any more errors.
+overlooked any other errors.
 
 > Finally, the conclusion and related work sections are reasonable.  I
 > think the conclusion could usefully discuss the executability of the
 > algorithm in the first half of the M-N proof.  
 
 Informally, the algorithm is clearly executable. But we have not 
-attempted this with our formalisation. 
+attempted this with our formalisation or modified the formalisation
+so that it becomes executable by Isabelle/HOL.
 
 > Also, the conclusion discusses the Brzozowski's algebraic method in 
 > this context, and argues that the equational constraints that appear