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 wider ...

  -- Lars

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