equal
deleted
inserted
replaced
80 text {* |
80 text {* |
81 The Isabelle \texttt{tty} tool provides a very interface for running |
81 The Isabelle \texttt{tty} tool provides a very interface for running |
82 the Isar interaction loop, with some support for command line |
82 the Isar interaction loop, with some support for command line |
83 editing. For example: |
83 editing. For example: |
84 \begin{ttbox} |
84 \begin{ttbox} |
85 isatool tty\medskip |
85 isabelle tty\medskip |
86 {\out Welcome to Isabelle/HOL (Isabelle2008)}\medskip |
86 {\out Welcome to Isabelle/HOL (Isabelle2008)}\medskip |
87 theory Foo imports Main begin; |
87 theory Foo imports Main begin; |
88 definition foo :: nat where "foo == 1"; |
88 definition foo :: nat where "foo == 1"; |
89 lemma "0 < foo" by (simp add: foo_def); |
89 lemma "0 < foo" by (simp add: foo_def); |
90 end; |
90 end; |