49 This provides an easy upgrade path for existing tactic scripts, as |
49 This provides an easy upgrade path for existing tactic scripts, as |
50 well as additional means for interactive experimentation and |
50 well as additional means for interactive experimentation and |
51 debugging of structured proofs. Isabelle/Isar supports a broad |
51 debugging of structured proofs. Isabelle/Isar supports a broad |
52 range of proof styles, both readable and unreadable ones. |
52 range of proof styles, both readable and unreadable ones. |
53 |
53 |
54 \medskip The Isabelle/Isar framework is generic and should work |
54 \medskip The Isabelle/Isar framework \cite{Wenzel:2006:Festschrift} |
55 reasonably well for any Isabelle object-logic that conforms to the |
55 is generic and should work reasonably well for any Isabelle |
56 natural deduction view of the Isabelle/Pure framework. Specific |
56 object-logic that conforms to the natural deduction view of the |
57 language elements introduced by the major object-logics are |
57 Isabelle/Pure framework. Specific language elements introduced by |
58 described in \chref{ch:hol} (Isabelle/HOL), \chref{ch:holcf} |
58 the major object-logics are described in \chref{ch:hol} |
59 (Isabelle/HOLCF), and \chref{ch:zf} (Isabelle/ZF). The main |
59 (Isabelle/HOL), \chref{ch:holcf} (Isabelle/HOLCF), and \chref{ch:zf} |
60 language elements are already provided by the Isabelle/Pure |
60 (Isabelle/ZF). The main language elements are already provided by |
61 framework. Nevertheless, examples given in the generic parts will |
61 the Isabelle/Pure framework. Nevertheless, examples given in the |
62 usually refer to Isabelle/HOL as well. |
62 generic parts will usually refer to Isabelle/HOL as well. |
63 |
63 |
64 \medskip Isar commands may be either \emph{proper} document |
64 \medskip Isar commands may be either \emph{proper} document |
65 constructors, or \emph{improper commands}. Some proof methods and |
65 constructors, or \emph{improper commands}. Some proof methods and |
66 attributes introduced later are classified as improper as well. |
66 attributes introduced later are classified as improper as well. |
67 Improper Isar language elements, which are marked by ``@{text |
67 Improper Isar language elements, which are marked by ``@{text |