For archival purposes, here are some past Isabelle tutorials from my old website at LRI (which will be discontinued eventually).
All posts by Makarius
Alexander Grothendieck
Born 28-Mar-1928 (Berlin, Germany), died 13-Nov-2014 (Saint-Lizier, France).
In my own studies, I have occasionally encountered the famous name of Grothendieck in lectures about functional analysis and logic. From a bit later, I remember discussions with Helmut Schwichtenberg about Tarski-Grothendieck set theory as the foundation of the formal mathematical language of Mizar.
In 2010, I came again across the name of Alexander Grothendieck several times, when searching the web about my new hometown Bures-sur-Yvette, where I lived until August 2014 only a few hundred meters from the famous IHÉS institute. That was the place where Grothendieck worked for some time at the peak of his mathematical life (until 1970). Afterwards he removed himself more and more from public and scientific life.
Winfried Scharlau has started to publish material about the life of Grothendieck some years ago, with this notable article from 2006/2008. There was also some activity on the web to collect more information, but this was stopped abruptly in 2010 with this angry letter from Grothendieck himself, speaking to the world from a secret place in the Pyrenees.
At least we now know that his last residence was in Lasserre (l’Ariège); see also this article of La Depeche.
Here is another blog with many more links.
Isabelle/PIDE as IDE for Standard ML
Strictly speaking the Isabelle environment is for interactive and automated theorem proving, but its SML IDE support is quite sophisticated: source files are statically checked and semantically evaluated while the user is editing. The annotated sources contain markup about inferred types, references to defining positions of items etc.
As a quick start, see the Documentation panel, section Examples, entry src/Tools/SML/Examples.thy (as of Isabelle2014).
The time where SML sources need to be edited with vi or emacs are over. See also this related thread on Stackoverflow.
Discontinuation of Isabelle Proof General
31-Oct-2014 is the historic date (Reformation Day!) when support for Proof General was ultimately removed from the Isabelle code base. This is the relevant changeset.
This means the current official release of Isabelle2014 (August 2014) is the last one where Proof General Emacs is still available as (optional) component; see the explanation in the published NEWS. After that its 15 years of history comes to an end, with the last 3 years an increasingly heavy burden and hindrance of further advances in Prover IDE technology (as represented by Isabelle/jEdit).
The TTY loop for the Isar toplevel has been removed as well, see changeset. It might appear rather drastic to have an Interactive Theorem Prover without the classic read-eval-print loop, but we need to recall that TTY interaction stems from the 1970-ies.
PIDE supports direct editing of theory documents as interactive sessions (or projects): this is more adequate for the interaction standards of the 1990-ies — a form of direct manipulation.
It should be noted that the general PIDE protocol infrastructure is sufficiently flexibile to support old-fashioned stepping through proof scripts as well, maybe even with some Emacs front-end. So Proof General veterans who do care enough about that may assemble at the proofgeneral-devel mailing list to prove that this old warrior is not-quite-dead yet.
UITP 2014 proceedings with Isabelle/jEdit paper
On 29-Oct-2014, EPTCS has published the proceedings of UITP 2014, which was a workshop at VSL 2014, Vienna, July 2014. The volume includes my contribution System description: Isabelle/jEdit in 2014. The paper has been updated to the current official release Isabelle2014 (August 2014).
Update of website, with included blog
After more than 10 years with a rather minimalistic website here at sketis.net, I have now activated the advanced Content Management System WordPress, which was part of the standard provider package. That was originally intended as blogging platform, which means there is now this easy to use way to warp sketis.net forwards in web-technology. But also vulnerability?