# [isabelle] Nominal Isabelle and pair types

`I am experimenting with using Nominal Isabelle for labelled deductive
``systems. For starters, I am trying to create a pair type of labels and
``formulae.
`
The following definition seems to work:
atom_decl simple_label prop_var
datatype formula = Atom "prop_var"
| Impl "formula" "formula"
| Conj "formula" "formula"
| Disj "formula" "formula"
| Bottom
nominal_datatype labelled_formula =
"\<guillemotleft>simple_label\<guillemotright> * formula"

`but them I am unable to use fst (and snd?) on the pair. I get type
``unification errors from the following:
`
constdefs
get_label :: "labelled_formula \<Rightarrow> simple_label"
"get_label lf \<equiv> (fst lf)"
get_formula :: "labelled_formula \<Rightarrow> formula"
"get_formula lf \<equiv> (snd lf)"
Please advise.
Thanks,
Rob

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