# [isabelle] Simple question about theory parameter

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?
Thanks,
Stephan

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