*To*: Dave Cunningham <dc04 at doc.ic.ac.uk>*Subject*: Re: [isabelle] discarding an assumption*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Wed, 21 Nov 2007 09:46:27 +1100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <20071120050322.GC7074@doc.ic.ac.uk>*References*: <20071120050322.GC7074@doc.ic.ac.uk>*User-agent*: Icedove 1.5.0.14pre (X11/20071018)

Dave Cunningham wrote:

Is it possible to delete an assumption from the current subgoal? While unnecessary, I sometimes find this useful while proving in proof general if the list of assumptions gets too big. Maybe this makes the proof space smaller while using the automatic methods too? I've been doing apply(erule_tac ?x="blah" in discard_assumption) where I've previously proved "discard_assumption" as [| ?x ; ?y |] ==> ?y but I'm assuming this is a bad idea. Isabelle certainly warns about it. Is there a better way? thanks

Dave, I can't see why it is a bad idea, except for the fact that your "discard_assumption" is in fact thin_rl, already in Isabelle. In fact the tactic thin_tac does exactly what you have done tactic.ML:fun thin_tac s = eres_inst_tac [("V",s)] thin_rl;

regards, Jeremy

**Follow-Ups**:**Re: [isabelle] discarding an assumption***From:*Dave Cunningham

**References**:**[isabelle] discarding an assumption***From:*Dave Cunningham

- Previous by Date: Re: [isabelle] [Code-Generation] 'No type arity (..)' - Problem
- Next by Date: [isabelle] Tools and Techniques for Verification of System Infrastructure (Announce)
- Previous by Thread: [isabelle] discarding an assumption
- Next by Thread: Re: [isabelle] discarding an assumption
- Cl-isabelle-users November 2007 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