Re: [isabelle] Novice question about functions

I have two suggestions. First, please base any set theory development on either Main_ZF or Main_ZFC, which contain full developments of axiomatic set theory, including in the latter case the axiom of choice. The theory ZF, which you currently use, contains only the raw axioms and should be regarded as an internal component of the implementation.

My other suggestion is that you avoid using locales until you have mastered the fundamentals of Isabelle.

Theorems appropriate to your development can be found in the theory func.thy. Use the magnifying glass tool to look for others.

Larry Paulson

On 15 Dec 2010, at 22:55, Victor Porton wrote:

> theory test
>   imports ZF
> begin
> locale subtest =
>   fixes move_fun::"i=>i"
>   fixes myset::i
> begin

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