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 MHonArc.