[isabelle] Unexpected Behavior with Sum_Type

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.


Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.