[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