Re: [isabelle] Unexpected Behavior with Sum_Type
On Sat, 2 Feb 2013, Alfio Martini wrote:
I would like to have a symbol in the completion pop up table for
disjoint union of sets "<+>". I suggest \<uplus> . I tried it myself,
but I kind of got lost with the dialog box. I wanted to add the
mathematical representation and not the internal Isabelle one.
Which dialog box do you mean?
The Isabelle/jEdit completions are derived from the cumulative "symbols"
specifications, notably $ISABELLE_HOME/etc/symbols and your
$ISABELLE_HOME_USER/etc/symbols (which is non-existent by default).
So if you put a line like this in the latter file it should work:
\<uplus> code: 0x00228e group: operator abbrev: <+>
This gives you physical rendering via Unicode and some input method, not
yet actual HOL notation, which is a different story.
This archive was generated by a fusion of
Pipermail (Mailman edition) and