[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:
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