From: Makarius <makarius@sketis.net>
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.
Makarius
From: Alfio Martini <alfio.martini@acm.org>
Dear Isabelle Users,
Isabelle2013-RC2 consider Projl a free variable in the following
expression:
value "Projl (Inl (3::nat))"
To get the right answer, I have to type
value "Sum_Type.Projl (Inl (3::nat))"
Even
lemma "Projl (Inl (3::nat)) = 3" by (simp add:Projl_Inl) does not work,
since Projl appears as a free variable.
Why does this happen, since Sum_Type is in Main?
I would not like to use the "Sum_Type" qualifier, if there is a workaround.
Also, if possible, 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.
Best!
From: Christian Sternagel <c.sternagel@gmail.com>
Dear Alfio,
I don't think that the unqualified Projl was ever visible. See also
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-July/msg00118.html
for a related thread.
The reason that those constants are not openly visible is the line
hide_const (open) Suml Sumr Projl Projr
at the end of Sum_Type.thy.
As Andreas pointed out in the thread above
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-July/msg00125.html
we can mostly replace Projl and Projr by case expressions.
cheers
chris
From: Alfio Martini <alfio.martini@acm.org>
Thanks for clarifying that Christian!!
Best!
Last updated: Mar 28 2024 at 16:17 UTC