[isabelle] Ambiguity warning with _lessAll and _setless_All



I get the following warning in Isabelle 2005:

### Ambiguous input "ALL y<(x::nat). P x"
### produces 2 parse trees.

### ("Trueprop" ("_lessAll" y ("_constrain" x nat) ("_applC" P x)))

### ("Trueprop" ("_setlessAll" y ("_constrain" x nat) ("_applC" P x)))

### Fortunately, only one parse tree is type correct.
### You may still want to disambiguate your grammar or your input.


Should I simply ignore it, or is there a way to turn it off (While still using the ALL y<x Syntax) ?

Greetings and thanks in advance
 Peter







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.