equal
deleted
inserted
replaced
16 constdefs foo :: nat "foo == 1"; |
16 constdefs foo :: nat "foo == 1"; |
17 lemma "0 < foo" by (simp add: foo_def); |
17 lemma "0 < foo" by (simp add: foo_def); |
18 end |
18 end |
19 \end{ttbox} |
19 \end{ttbox} |
20 Note that any Isabelle/Isar command may be retracted by \texttt{undo}. See |
20 Note that any Isabelle/Isar command may be retracted by \texttt{undo}. See |
21 the Isabelle/Isar Quick Reference (Appendix~{ap:refcard}) for a comprehensive |
21 the Isabelle/Isar Quick Reference (Appendix~\ref{ap:refcard}) for a |
22 overview of available commands and other language elements. |
22 comprehensive overview of available commands and other language elements. |
23 |
23 |
24 |
24 |
25 \subsection{Proof~General} |
25 \subsection{Proof~General} |
26 |
26 |
27 Plain TTY-based interaction as above used to be quite feasible with |
27 Plain TTY-based interaction as above used to be quite feasible with |