For archival purposes, here are some past Isabelle tutorials from my old website at LRI (which will be discontinued eventually).
Category Archives: Isabelle
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).