abbreviation (output)
leq_le :: "int => int => int => bool" ("_ ≤ _ < _")
where
"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?
Tobias
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
