--- a/LMCS-Review	Mon Jan 09 10:12:46 2012 +0000
+++ b/LMCS-Review	Mon Jan 09 10:45:12 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 
@@ -188,6 +203,18 @@
 >   of pairs. I think that the system should at the very least allow encoding
 >   this example, otherwise set-abstractions will not be very useful in
 >   practice.
+
+>> datatype trm =
+>>       Var string
+>>     | App trm trm
+>>     | Lam string trm
+>>     | Let "(string * trm) fset" trm
+>> Not a problem. Both finite sets and bags should be possible as
+>> constructors within the new package.
+>> Best regards and a happy new year!
+>> Andrei Popescu
+
+
 >
 > Detailed comments
 >