*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] subst question*From*: Jeremy Dawson <Jeremy.Dawson at rsise.anu.edu.au>*Date*: Thu, 13 Oct 2005 12:21:52 +1000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <Pine.LNX.4.58.0510121209500.7291@atbroy65.informatik.tu-muenchen.de>*Organization*: Australian National University*References*: <DF61E1D8-6295-436B-9E45-AE30565F7344@acm.org> <434C3FFC.30305@rsise.anu.edu.au> <Pine.LNX.4.58.0510121209500.7291@atbroy65.informatik.tu-muenchen.de>*User-agent*: Mozilla Thunderbird 0.9 (X11/20041124)

Makarius wrote:

On Wed, 12 Oct 2005, Jeremy Dawson wrote:by (PRIMITIVE standard) ; by (instantiate_tac [("y", "fst")]) ;Just note that using standard within a proof is a very bad idea -- its purpose is to conclude a sequence of reasoning, producing a certain normal form with some internal rearrangements. Even worse, standard only works properly in a top-level theory context, but messes up the proof state in the presence of local assumptions, locales etc.

> Makarius

Alternatively to using standard, do by (PRIMITIVE zero_var_indexes) ; This has less effect on the remainder of the proof state, in particular it doesn't turn hypotheses of the proof state into premises Jeremy

**References**:**[isabelle] subst question***From:*Reto Kramer

**Re: [isabelle] subst question***From:*Jeremy Dawson

**Re: [isabelle] subst question***From:*Makarius

- Previous by Date: [isabelle] TPHOLs 2007: Call for bids
- Next by Date: [isabelle] AFP 2005
- Previous by Thread: Re: [isabelle] subst question
- Next by Thread: [isabelle] (no subject)
- Cl-isabelle-users October 2005 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