49 This provides an easy upgrade path for existing tactic scripts, as |
47 This provides an easy upgrade path for existing tactic scripts, as |
50 well as additional means for interactive experimentation and |
48 well as additional means for interactive experimentation and |
51 debugging of structured proofs. Isabelle/Isar supports a broad |
49 debugging of structured proofs. Isabelle/Isar supports a broad |
52 range of proof styles, both readable and unreadable ones. |
50 range of proof styles, both readable and unreadable ones. |
53 |
51 |
54 \medskip The Isabelle/Isar framework \cite{Wenzel:2006:Festschrift} |
52 \medskip The generic Isabelle/Isar framework (see |
55 is generic and should work reasonably well for any Isabelle |
53 \chref{ch:isar-framework}) should work reasonably well for any |
56 object-logic that conforms to the natural deduction view of the |
54 Isabelle object-logic that conforms to the natural deduction view of |
57 Isabelle/Pure framework. Specific language elements introduced by |
55 the Isabelle/Pure framework. Specific language elements introduced |
58 the major object-logics are described in \chref{ch:hol} |
56 by the major object-logics are described in \chref{ch:hol} |
59 (Isabelle/HOL), \chref{ch:holcf} (Isabelle/HOLCF), and \chref{ch:zf} |
57 (Isabelle/HOL), \chref{ch:holcf} (Isabelle/HOLCF), and \chref{ch:zf} |
60 (Isabelle/ZF). The main language elements are already provided by |
58 (Isabelle/ZF). The main language elements are already provided by |
61 the Isabelle/Pure framework. Nevertheless, examples given in the |
59 the Isabelle/Pure framework. Nevertheless, examples given in the |
62 generic parts will usually refer to Isabelle/HOL as well. |
60 generic parts will usually refer to Isabelle/HOL as well. |
63 |
61 |