[isabelle] Mysterious behavior of "let"



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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.