equal
deleted
inserted
replaced
25 * \<bullet> is now output as bold \cdot by default, which looks much |
25 * \<bullet> is now output as bold \cdot by default, which looks much |
26 better in printed text; |
26 better in printed text; |
27 |
27 |
28 * added default LaTeX bindings for \<tturnstile> and \<TTurnstile>; |
28 * added default LaTeX bindings for \<tturnstile> and \<TTurnstile>; |
29 note that these symbols are currently unavailable in Proof General / |
29 note that these symbols are currently unavailable in Proof General / |
30 X-Symbol; |
30 X-Symbol; added \<euro> symbol; |
|
31 |
|
32 * isatool latex no longer depends on changed TEXINPUTS, instead |
|
33 isatool document copies the Isabelle style files to the target |
|
34 location; |
31 |
35 |
32 |
36 |
33 *** Isar *** |
37 *** Isar *** |
34 |
38 |
35 * Pure/Provers: improved proof by cases and induction; |
39 * Pure/Provers: improved proof by cases and induction; |
239 |
243 |
240 * HOL/IMP: updated and converted to new-style theory format; several |
244 * HOL/IMP: updated and converted to new-style theory format; several |
241 parts turned into readable document, with proper Isar proof texts and |
245 parts turned into readable document, with proper Isar proof texts and |
242 some explanations (by Gerwin Klein); |
246 some explanations (by Gerwin Klein); |
243 |
247 |
|
248 * HOL-Hyperreal is now a logic image; |
|
249 |
244 |
250 |
245 *** HOLCF *** |
251 *** HOLCF *** |
246 |
252 |
247 * Isar: consts/constdefs supports mixfix syntax for continuous |
253 * Isar: consts/constdefs supports mixfix syntax for continuous |
248 operations; |
254 operations; |