63 section {* Quick start *} |
63 section {* Quick start *} |
64 |
64 |
65 subsection {* Terminal sessions *} |
65 subsection {* Terminal sessions *} |
66 |
66 |
67 text {* |
67 text {* |
68 Isar is already part of Isabelle. The low-level @{verbatim |
68 The Isabelle \texttt{tty} tool provides a very interface for running |
69 isabelle} binary provides option @{verbatim "-I"} to run the |
69 the Isar interaction loop, with some support for command line |
70 Isabelle/Isar interaction loop at startup, rather than the raw ML |
70 editing. For example: |
71 top-level. So the most basic way to do anything with Isabelle/Isar |
71 \begin{ttbox} |
72 is as follows: % FIXME update |
72 isatool tty\medskip |
73 \begin{ttbox} |
73 {\out Welcome to Isabelle/HOL (Isabelle2008)}\medskip |
74 isabelle -I HOL\medskip |
|
75 \out{> Welcome to Isabelle/HOL (Isabelle2005)}\medskip |
|
76 theory Foo imports Main begin; |
74 theory Foo imports Main begin; |
77 definition foo :: nat where "foo == 1"; |
75 definition foo :: nat where "foo == 1"; |
78 lemma "0 < foo" by (simp add: foo_def); |
76 lemma "0 < foo" by (simp add: foo_def); |
79 end; |
77 end; |
80 \end{ttbox} |
78 \end{ttbox} |
81 |
79 |
82 Note that any Isabelle/Isar command may be retracted by @{command |
80 Any Isabelle/Isar command may be retracted by @{command "undo"}. |
83 "undo"}. See the Isabelle/Isar Quick Reference |
81 See the Isabelle/Isar Quick Reference (\appref{ap:refcard}) for a |
84 (\appref{ap:refcard}) for a comprehensive overview of available |
82 comprehensive overview of available commands and other language |
85 commands and other language elements. |
83 elements. |
86 *} |
84 *} |
87 |
85 |
88 |
86 |
89 subsection {* Proof General *} |
87 subsection {* Proof General *} |
90 |
88 |