[isabelle-dev] abbreviation (output)
nipkow at in.tum.de
Thu Jan 23 15:20:58 CET 2014
leq_le :: "int => int => int => bool" ("_ ≤ _ < _")
"a ≤ b < c == a ≤ b & b < c"
This used to work until recently, but now (parent: 55123:a389b50e6a42 tip) I get
*** Inner syntax error: unexpected end of input
It looks like the annotation ("_ ≤ _ < _") is ignored. If I remove (output) it
works again. What am I doing wrong?
More information about the isabelle-dev