equal
deleted
inserted
replaced
45 |
45 |
46 * Communication with Proof General is now 8bit clean, which means that |
46 * Communication with Proof General is now 8bit clean, which means that |
47 Unicode text in UTF-8 encoding may be used within theory texts (both |
47 Unicode text in UTF-8 encoding may be used within theory texts (both |
48 formal and informal parts). Cf. option -U of the Isabelle Proof |
48 formal and informal parts). Cf. option -U of the Isabelle Proof |
49 General interface; HOL/ex/Hebrew.thy provides a simple example. |
49 General interface; HOL/ex/Hebrew.thy provides a simple example. |
|
50 |
|
51 * Improved efficiency of the Simplifier and, to a lesser degree, the |
|
52 Classical Reasoner. Typical big applications run around 2 times |
|
53 faster. |
50 |
54 |
51 |
55 |
52 *** Document preparation *** |
56 *** Document preparation *** |
53 |
57 |
54 * Commands 'display_drafts' and 'print_drafts' perform simple output |
58 * Commands 'display_drafts' and 'print_drafts' perform simple output |