*** 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).
* Addi
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 Jenkins
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 of the negated quantifier (by
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. P
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
> fi
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, "isabelle-de