Re: [isabelle] "and similarly..."
On 31.01.2012 16:57, John Wickerson wrote:
Is there a feature in Isabelle that corresponds to writing "and similarly" in an informal pen-and-paper proof? Specifically, here is a fragment of my proof script:
Apart from adhoc-mechanisms on the ML level, there is no such thing in
Isabelle. There have been occasional requests for support of concepts
like 'proof by analogy' or 'without loss of generality'. But to my
knowledge, there haven't been any efforts to implement such a thing.
Support for the really simple cases (like your example, just replace
HeadMap by TailMap everwhere) would probably be just a technical
problem, but often the mathematical notion of "similarly" is quite a bit
This archive was generated by a fusion of
Pipermail (Mailman edition) and