[isabelle] Feature suggestion: matching arguments by a unique tag



After some experimentation I concluded that Isabelle 2011 does not support definitions of functions with pattern matching by a unique tag. For example the following does not work:

typedecl tag

consts t1::tag
consts t2::tag

definition "f (t1, x) = t1"
definition "f (t2, x) = t2"

I think it is a good idea to make this working in a future version of Isabelle (or in an entirely new proof assistant).

-- 
Victor Porton - http://portonvictor.org





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