author | wenzelm |

Tue Apr 13 20:31:55 2004 +0200 (2004-04-13) | |

changeset 14556 | c5078f6c99a9 |

parent 14555 | 341908d6c792 |

child 14557 | 31ae4a47267c |

* Calculation commands "moreover" and "also" no longer interfere with

current facts ("this"), admitting arbitrary combinations with "then"

and derived forms.

current facts ("this"), admitting arbitrary combinations with "then"

and derived forms.

1.1 --- a/NEWS Tue Apr 13 20:22:26 2004 +0200 1.2 +++ b/NEWS Tue Apr 13 20:31:55 2004 +0200 1.3 @@ -10,7 +10,7 @@ 1.4 Replaces linorder.ML. 1.5 1.6 * Pure: Greek letters (except small lambda, \<lambda>), as well as gothic 1.7 - (\<aa>...\<zz>\<AA>...\<ZZ>), caligraphic (\<A>...\<Z>), and euler 1.8 + (\<aa>...\<zz>\<AA>...\<ZZ>), calligraphic (\<A>...\<Z>), and euler 1.9 (\<a>...\<z>), are now considered normal letters, and can therefore 1.10 be used anywhere where an ASCII letter (a...zA...Z) has until 1.11 now. COMPATIBILITY: This obviously changes the parsing of some 1.12 @@ -54,6 +54,7 @@ 1.13 (somewhat) independet of content. It is copied from lib/html/isabelle.css. 1.14 It can be changed to alter the colors/layout of generated pages. 1.15 1.16 + 1.17 *** Isar *** 1.18 1.19 * Tactic emulation methods rule_tac, erule_tac, drule_tac, frule_tac, 1.20 @@ -72,8 +73,9 @@ 1.21 theorems to have too special types in some circumstances. 1.22 - "where" permits explicit instantiations of type variables. 1.23 1.24 -* Calculation commands "moreover" and "also": 1.25 - Do not reset facts ("this") any more. 1.26 +* Calculation commands "moreover" and "also" no longer interfere with 1.27 + current facts ("this"), admitting arbitrary combinations with "then" 1.28 + and derived forms. 1.29 1.30 * Locales: 1.31 - Goal statements involving the context element "includes" no longer 1.32 @@ -100,6 +102,7 @@ 1.33 * HOL: Tactic emulation methods induct_tac and case_tac understand static 1.34 (Isar) contexts. 1.35 1.36 + 1.37 *** HOL *** 1.38 1.39 * Simplifier: