*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Prove by instantiation*From*: John Munroe <munddr at gmail.com>*Date*: Wed, 6 Oct 2010 17:36:26 +0200

Hello For the following: axiomatization c :: real where ax1 : "c > 0" lemma "EX z. c = z" sorry Can the quantifier be proved by instantiation only? Perhaps, this question logically follows: is there an expression y such that apply (rule exI [where x=y])? Thank you for the help. John

**Follow-Ups**:**Re: [isabelle] Prove by instantiation***From:*Joachim Breitner

- Previous by Date: [isabelle] case_names and consumes
- Next by Date: Re: [isabelle] G.U.T.
- Previous by Thread: [isabelle] case_names and consumes
- Next by Thread: Re: [isabelle] Prove by instantiation
- Cl-isabelle-users October 2010 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