On Wed, 4 Apr 2012, Rob Arthan wrote:
On 4 Apr 2012, at 11:48, David Matthews wrote:
On 03/04/2012 16:20, Rob Arthan wrote:
On 30 Mar 2012, at 12:52, David Matthews wrote:
Looking carefully at the syntax, though, "op" is not allowed in a
datatype specification although in all other respects the syntax of
a binding and a specification are the same. I've added an error
message if "op" is used in a specification.
I didn't look at the syntax of modules. You are quite right. In fact,
as far as I can see, op is not allowed anywhere in a signature.
I've now reduced the error message to a warning since it seems Isabelle
has "op" in signatures.
Tut, tut :-). Somewhat to my surprise, the ProofPower source does comply
with the standard syntax, even though I was completely unaware that "op"
wasn't allowed in signatures.
Historically, we've always tried to minimize the problems in the grey
areas of the SML standard, with its occasional changes that were not
immediately clear from outside.
I have no problems to remove inappropriate "op" occurrences from the
Isabelle sources, if it does not break SML/NJ or old versions of Poly/ML
(5.2.1, 5.3.0, 5.4.x). On the other hand it will make testing of old
Isabelle versions with brand new Poly/ML versions more difficult.
Makarius
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
