*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Domain proof*From*: Peter Lammich <lammich at in.tum.de>*Date*: Fri, 17 Jan 2014 17:34:01 +0100*In-reply-to*: <DUB124-W2BC80B14532550F749C8D8FB80@phx.gbl>*References*: <DUB124-W2BC80B14532550F749C8D8FB80@phx.gbl>

On Fr, 2014-01-17 at 18:03 +0200, Roger H. wrote: > Hi, > > how can i prove > > lemma "dom (SOME b. dom b = A) = A" > You have to show that there is such a beast b, ie, proof - obtain b where "dom b = A" ... thus ?thesis sledgehammer (*Should find a proof now, using the rules for SOME, probably SomeI*) -- Peter > Thank you! >

**Follow-Ups**:**Re: [isabelle] Domain proof***From:*Manuel Eberl

**References**:**[isabelle] Domain proof***From:*Roger H .

- Previous by Date: [isabelle] Domain proof
- Next by Date: Re: [isabelle] Domain proof
- Previous by Thread: [isabelle] Domain proof
- Next by Thread: Re: [isabelle] Domain proof
- Cl-isabelle-users January 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list