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.

Tobias

> Thanks,
> Stephan





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