Re: [isabelle] includes bundle works only in first case

Hi Makarius,

thanks for the explanation.

So yes, it is all within the normal parameters of Isar, despite the potential
surprise. The above example indicates that the new 'including' command is better
not used before a proof block. BTW, the longer existing 'using', with its later
addition to affect the context, already produces the same effect:

lemma "x = x" "y = y"
using [[show_types]]
show "y = y" ..
I have never tried this. So far, I only used "using <facts>" and "unfolding <some_def>". The latter always worked on all goals and the former affected all goals if used with the right initial method (-, simp_all, auto, etc.), so I would have expected that something similar applies to including.

In the example above you are using 'next' as if would "separate subgoals", but
this is not really its meaning. Plain 'show' statements do not have to be
In my real use case, each goal had the full fix-assume-show chain, so the next was necessary there.

Here is an alternative form that includes a bundle in the context of a toplevel

includes test
shows "test xs = []" and "test ys = []"
proof -
show "test xs = []" by simp
next -- "redundant"
show "test ys = []" by simp
I read about that alternative, but I actually prefer "including" over "includes", because including does not clutter the statement of the lemma with hints to the prover.


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