[isabelle-dev] Safe approach to hypothesis substitution mark II

[Thomas Sewell]

Whoops.

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

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