[isabelle-dev] Safe approach to hypothesis substitution mark II
thomas.sewell at nicta.com.au
Thu Jan 16 02:02:45 CET 2014
It's both a typo and use of the wrong release.
The patch happens to work against Isabelle2013-1 or Isabelle2013-2,
since there are no relevant differences in the theory sources. I can
confirm that isabelle build -a works in either 2013-1 or 2013-2.
Short version of the story, I forgot the name of the newest release.
Long version: The confusion was caused in part because the newest
l4.verified branch is called '2013-1'. It contains Isabelle 2013-2, but
the switch was accomplished so straightforwardly that we didn't end up
with a new branch name.
Apologies about the confusion,
On 16/01/14 02:00, Makarius wrote:
> On Tue, 14 Jan 2014, Thomas Sewell wrote:
>> This is also a patch against Isabelle2013-1.
> Is that just a typo, or are you still using that failed release? The
> current one is Isabelle2013-2, and it does not introduce any
> incompatibilities over Isabelle2013-1, so there is no reason to keep
> using that.
More information about the isabelle-dev