Une session ISABELLE commence en tapant isabelle
dans une fenêtre système. Il s'agit en fait d'un
interprète ML
(le langage fonctionnel dont dérive CAML) avec
un certain nombre
de fonctions prédéfinies pour la preuve de
théorèmes
- quitter par Ctrl+D ou quit();.