Re: [isabelle-dev] Circular reasoning via multithreading seems too easy

2016-12-04 Thread Lars Hupel
> 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). _

Re: [isabelle-dev] Circular reasoning via multithreading seems too easy

2016-12-04 Thread Peter Lammich
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

Re: [isabelle-dev] Circular reasoning via multithreading seems too easy

2016-12-04 Thread Makarius
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

Re: [isabelle-dev] Circular reasoning via multithreading seems too easy

2016-12-04 Thread Lars Hupel
>> 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. ___

Re: [isabelle-dev] Circular reasoning via multithreading seems too easy

2016-12-04 Thread Peter Lammich
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

Re: [isabelle-dev] Circular reasoning via multithreading seems too easy

2016-12-04 Thread Makarius
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