*To*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] Mysterious behavior of "let"*From*: "Eugene W. Stark" <isabelle-users at starkeffect.com>*Date*: Sun, 25 Sep 2016 06:43:32 -0400*Reply-to*: stark at cs.stonybrook.edu*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.2.0

Can somebody explain this mysterious behavior? Thanks. - Gene Stark ---------------------- theory Barf imports Main begin lemma shows nothing proof - let ?x0 = 100 let ?x1 = 101 let ?y = "\<lambda>i. if i = 0 then ?x0 else ?x1" have "?y 0 = ?x0" by presburger let ?x = 102 have "?y 0 = ?x0" oops (* ?x0 is now 102 *) end

theory Barf imports Main begin lemma shows nothing proof - let ?x0 = 100 let ?x1 = 101 let ?y = "\<lambda>i. if i = 0 then ?x0 else ?x1" have "?y 0 = ?x0" by presburger let ?x = 102 have "?y 0 = ?x0" oops (* ?x0 is now 102 *) end

**Follow-Ups**:**Re: [isabelle] Mysterious behavior of "let"***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Structuring a Modular Project
- Next by Date: Re: [isabelle] Mysterious behavior of "let"
- Previous by Thread: [isabelle] Fwd: Re: case rule and OF
- Next by Thread: Re: [isabelle] Mysterious behavior of "let"
- Cl-isabelle-users September 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