Re: [isabelle] Unexpected Behavior with Sum_Type
I don't think that the unqualified Projl was ever visible. See also
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
we can mostly replace Projl and Projr by case expressions.
On 02/03/2013 01:55 AM, Alfio Martini wrote:
Dear Isabelle Users,
Isabelle2013-RC2 consider Projl a free variable in the following
value "Projl (Inl (3::nat))"
To get the right answer, I have to type
value "Sum_Type.Projl (Inl (3::nat))"
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and