On Thu, 10 Mar 2016, Florian Haftmann wrote:
in 66a381d3f88f, the usual syntax for big operators has been added for
GCD (and LCM):
(a) Gcd x \ A. f x
An alternative could be
(b) GCD x \ A. f x
The form (b) follows the tradition to have binders all-capitalized (SUP,
INF, UNION, INTER, THE,
On Thu, 7 Apr 2016, Makarius wrote:
*** Prover IDE -- Isabelle/Scala/jEdit ***
* IDE support for the Isabelle/Pure bootstrap process.
After further refinements (e.g. see current Isabelle/79f41fbdf74a), the
Pure IDE bootstrap works even more smoothly. In particular it can be
combined with
