[isabelle] includes bundle works only in first case



Hi all,

I stumbled across the following (unexpected) behaviour: If I do an Isar proof of multiple goals I have refined the proof state by including a bundle prior to the opening "proof", the "next" separator deletes the bundle.

Here's an example:

definition test :: "'a list => 'a list" where "test xs = []"
bundle test = test_def[simp]
lemma shows "test xs = []" and "test ys = []"
  including test
proof -
  show "test xs = []" by simp
next
  show "test ys = []" by simp (* fails *)
qed

Surprisingly, it works if I nest the multiple goals inside a block:

proof -
  {
    show "test xs = []" by simp
  next
    show "test ys = []" by simp (* works *)
  }
qed

Is this behaviour intended?

Andreas

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft





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