Re: [isabelle] Proof by analogy and proof stability in Isabelle

I might summarize it this way: Locale interpretation transforms a
generic theory into a concrete one. What we're looking for is a way to
transform a *concrete* theory into a *different* concrete one (or a
new generic one, as the case may be).
- Brian

It seems to me the way mathematics usually works is to take the concrete, abstract it, and THEN ONLY apply it to something different concrete.

- Steven

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