*To*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] Using an assumption as a rule*From*: Edward Pierzchalski <e.a.pierzchalski at gmail.com>*Date*: Thu, 06 Oct 2016 09:50:51 +0000

Hi all, Say my current goal looks like: A v ==> (!! x. B x ==> C x) ==> C v Here, I have an assumption that I could easily use as an introduction rule for my conclusion, resulting in the new goal A v ==> B v ==> C v If I were in Isar mode, the rule-shaped assumption would have a name that I could apply using the rule tactic. Is there an easy way to do this in apply mode? At the moment I'm repeatedly using meta_allE (my case has a few more bound variables), but this seems dirty. Regards, --Ed

**Follow-Ups**:**Re: [isabelle] Using an assumption as a rule***From:*Simon Wimmer

- Previous by Date: Re: [isabelle] Help defining a mutually recursive function
- Next by Date: Re: [isabelle] Using an assumption as a rule
- Previous by Thread: Re: [isabelle] Help defining a mutually recursive function
- Next by Thread: Re: [isabelle] Using an assumption as a rule
- Cl-isabelle-users October 2016 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