> Where did you see these lots of Unsynchronized.ref (or better
> Synchronized.var) in Isabelle Tools?
There are 48 occurrences of "Unsynchronized.ref" in "~~/src/Tools", 181
in "~~/src/HOL", and some more in the AFP (many of which appear to be in
generated code).
_
This was an artificial counterexample, which I tried out of curiosity, but having applications like caching of already proved theorems in mind.Peter Originalnachricht Betreff: Re: [isabelle-dev] Circular reasoning via multithreading seems too easyVon: Makarius An: Peter Lammich ,isa
On 04/12/16 11:14, Lars Hupel wrote:
>> Where did you see these lots of Unsynchronized.ref (or better
>> Synchronized.var) in Isabelle Tools?
>
> There are 48 occurrences of "Unsynchronized.ref" in "~~/src/Tools", 181
> in "~~/src/HOL", and some more in the AFP (many of which appear to be in
> gen
>> There are 48 occurrences of "Unsynchronized.ref" in "~~/src/Tools", 181
>> in "~~/src/HOL", and some more in the AFP (many of which appear to be in
>> generated code).
>
> So what is wrong here?
Nothing, as far as I am concerned. I was merely trying to answer your
question.
___
On So, 2016-12-04 at 22:30 +0100, Makarius wrote:
> On 04/12/16 11:14, Lars Hupel wrote:
> >
> > >
> > > Where did you see these lots of Unsynchronized.ref (or better
> > > Synchronized.var) in Isabelle Tools?
> > There are 48 occurrences of "Unsynchronized.ref" in "~~/src/Tools",
> > 181
> > in
On 04/12/16 22:52, Peter Lammich wrote:
> On So, 2016-12-04 at 22:30 +0100, Makarius wrote:
>> On 04/12/16 11:14, Lars Hupel wrote:
>>>
Where did you see these lots of Unsynchronized.ref (or better
Synchronized.var) in Isabelle Tools?
>>> There are 48 occurrences of "Unsynchronized.r