Re: [isabelle] I want to print axiomatization info



On 8 Jul 2012, at 02:18, Gottfried Barrow wrote:

> 2) I got lots of warnings like: "Ambiguous input produces 4 parse trees... Fortunately, only one parse tree is type correct..."

This message indicates that your syntax is ambiguous. The way to eliminate such a message is by disambiguating your syntax, which in most cases means tightening up the precedences of operators. And indeed, your operator “in" gives no precedence information for its operands. I wonder why you don't use something akin to (ignoring fancy symbols)

	(infixl "IN" 55)

where you have

	("_ IN_ " 55) .

Larry Paulson








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