*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] schematic variables and assumption*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Date*: Tue, 15 May 2012 14:31:47 +0300*In-reply-to*: <4FB22629.4000202@in.tum.de>*References*: <4FB22629.4000202@in.tum.de>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.7; rv:12.0) Gecko/20120428 Thunderbird/12.0.1

Hello, I have the following lemma: lemma "(¬ (∀ x . P x)) ⟹ (∃ x . ¬ P x)" apply (rule exI) apply (rule notI) apply (erule notE) apply (rule allI) apply assumption After the the rule "apply (rule allI)" the goal becomes: ⋀x. P ?x ⟹ P x I do not understand why "apply assumption" fail at this point. I would expect that ?x is unified with x and the proof succeed. Best regards, Viorel Preoteasa

**Follow-Ups**:**Re: [isabelle] schematic variables and assumption***From:*Lawrence Paulson

**Re: [isabelle] schematic variables and assumption***From:*Alfio Martini

**References**:**[isabelle] jedit***From:*Tobias Nipkow

- Previous by Date: [isabelle] jedit
- Next by Date: Re: [isabelle] schematic variables and assumption
- Previous by Thread: [isabelle] jedit
- Next by Thread: Re: [isabelle] schematic variables and assumption
- Cl-isabelle-users May 2012 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