On 03/12/16 14:57, Peter Lammich wrote:
>
> 2. Is there any simple coding policy that guarantees absence of such
> problems? Would be: "Do not store cterm/thm + everything containing it
> in references" enough, or perhaps: "Do not use Unsynchronized.ref at
> all"? (There are lots of usages of
On 03/12/16 14:57, Peter Lammich wrote:
>
> the attached theory is accepted by all Isabelle's from 2015 to the
> latest 2016-1-RC4, without any complaints, even in batch mode
> (isabelle build).
> It just uses a prove_future, and proves the theorem with itself!
The behaviour is the same in
Hi all,
the attached theory is accepted by all Isabelle's from 2015 to the
latest 2016-1-RC4, without any complaints, even in batch mode
(isabelle build).
It just uses a prove_future, and proves the theorem with itself!
So, I have two questions here:
1. I always thought that there is some
