[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
  show "test ys = []" by simp (* fails *)

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

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

Is this behaviour intended?


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
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.