[isabelle-dev] NEWS: abbrevs and symbols dockable

2016-09-14 Thread Makarius
*** Prover IDE -- Isabelle/Scala/jEdit *** * Dockable window "Symbols" also provides access to 'abbrevs' from the outer syntax of the current theory buffer. This provides clickable syntax templates, including entries with empty abbrevs name (which are inaccessible via keyboard completion). *

[isabelle-dev] Jenkins maintenance

2016-09-14 Thread Lars Hupel
Dear Isabelle developers, over the weekend, there will be – once again – a scheduled maintenance on the build infrastructure. I will add some more jobs (which are running nightly) to test a wider variety of side conditions (mainly -j/-o threads). I will take this opportunity to tidy up the

Re: [isabelle-dev] not-exists problem

2016-09-14 Thread Lawrence Paulson
The symmetry between the variables in ~(∃x y. P x y) is completely lost in ∄x. ∃y. P x y. It’s a terrible notation. Larry > On 13 Sep 2016, at 22:56, Jasmin Blanchette > wrote: > >> I’m not sure that this suggestion addresses my original problem: that the >> use

Re: [isabelle-dev] not-exists problem

2016-09-14 Thread Michael.Norrish
Note that ∃!x. ∃!y. P x y is not equivalent to ∃!xy. P (fst xy) (snd xy). If you were going to support ∃!x y at all (and I can certainly see the argument for forbidding it outright), I'd expect it to map to the first formula above, and not the second. Michael On 13/09/2016, 18:41,

Re: [isabelle-dev] not-exists problem

2016-09-14 Thread Tobias Nipkow
This discussion clearly shows that ∃! with multiple bound variables is a recipe for confusion and should be avoided. Tobias On 14/09/2016 09:49, Peter Lammich wrote: On Di, 2016-09-13 at 23:35 +, michael.norr...@data61.csiro.au wrote: Note that ∃!x. ∃!y. P x y is not equivalent to ∃!xy.

Re: [isabelle-dev] not-exists problem

2016-09-14 Thread Peter Lammich
On Di, 2016-09-13 at 23:35 +, michael.norr...@data61.csiro.au wrote: > Note that ∃!x. ∃!y. P x y is not equivalent to ∃!xy. P (fst xy) (snd > xy). > > If you were going to support ∃!x y at all (and I can certainly see > the argument for forbidding it outright), I'd expect it to map to the >