Re: [isabelle] Simple question about theory parameter

Am 23/07/2012 15:12, schrieb Stephan van Staden:
> Dear all,
> Here is a simplified version of my problem, which should have a simple answer.
> I wish to prove a bunch of theorems about an arbitrary set S of numbers that
> contains a designated element, say 1. For example, S intersect S and S union S
> will both contain 1, etc.
> Thereafter, I wish to get theorems for free about particular sets that contain
> 1. For example, {1,2,3} intersect {1,2,3} contains 1, etc.
> What is the recommended way to do this in Isabelle?

It sounds like locales could be the answer.


> Thanks,
> Stephan

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