equal
deleted
inserted
replaced
57 |
57 |
58 * new Isabelle/Isar subsystem provides an alternative to traditional |
58 * new Isabelle/Isar subsystem provides an alternative to traditional |
59 tactical theorem proving; together with the ProofGeneral/isar user |
59 tactical theorem proving; together with the ProofGeneral/isar user |
60 interface it offers an interactive environment for developing human |
60 interface it offers an interactive environment for developing human |
61 readable proof documents (Isar == Intelligible semi-automated |
61 readable proof documents (Isar == Intelligible semi-automated |
62 reasoning); see isatool doc isar-ref and |
62 reasoning); actual document preparation based on (PDF)LaTeX is |
63 http://isabelle.in.tum.de/Isar/ for more information; |
63 available as well; see isatool doc isar-ref, HOL/Isar_examples and |
|
64 http://isabelle.in.tum.de/Isar/ for more information. |
64 |
65 |
65 * native support for Proof General, both for classic Isabelle and |
66 * native support for Proof General, both for classic Isabelle and |
66 Isabelle/Isar (the latter is slightly better supported and more |
67 Isabelle/Isar (the latter is slightly better supported and more |
67 robust); |
68 robust); |
68 |
69 |