diff -r 09acd7e116e8 -r 5b5ade6bc889 LMCS-Review
--- a/LMCS-Review	Thu Dec 29 18:05:13 2011 +0000
+++ b/LMCS-Review	Mon Jan 02 16:13:16 2012 +0000
@@ -49,7 +49,11 @@
 > algorithm W [...]."  But there is no analysis in the paper of what was
 > hard in algorithm W coded with single binders, or explanation of how
 > it would be done in the new system reported in this paper showing why
-> the new approach works better in practice.  Although this example is
+> the new approach works better in practice.  
+
+Added
+
+> Although this example is
 > one of the main motivations given for the work, there is apparently no
 > formalization of algorithm W in the library of examples that comes
 > with Nominal2 described in this paper.  I think that should be
@@ -59,24 +63,35 @@
 > binding single variables have not fared extremely well with the more
 > advanced tasks in the POPLmark challenge [2], because also there one
 > would like to bind multiple variables at once.").
->
+
+No time to provide full examples yet. They will be provided
+once Nominal2 becomes more mature and people are using it
+and help to provide theories.
+
 > The new Isabelle package "Nominal2", described in this paper, is not
 > ready for users without a lot of hand-holding from the Nominal2
 > developers.  This paper would have more impact if interested users
 > could try the tool without so much difficulty.
->
+
+The plan is to have Nominal Isabelle be part of the next stable 
+release of Isabelle, which should be out before the summer 2012.
+At the moment it can be downloaded as a bundle and is ready
+to be used (we have confirmation from two groups for this). 
+
 > A few more specific points:
 >
 > Bottom of p.7: I don't understand the paragraph containing equations
 > (2.4) and (2.5).
->
+
+
 > Bottom of p.9: The parameters R and fa of the alpha equivalence
 > relation are dropped in the examples, so the examples are not clear.
 > I think there is a typo in the first example: "It can be easily
 > checked that ({x,y},x->y) and ({y,x},y->x) are alpha-equivalent [...]"
 > Did you mean "({x,y},x->y) and ({y,x},x->y) are alpha-equivalent"?
->
->
+
+
+
 > Referee no 2:
 >
 >  * The paper can be accepted for Logical Methods in Computer Science