[isabelle] Unexpected Behavior with Sum_Type



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!

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