equal
deleted
inserted
replaced
|
1 |
1 Isabelle NEWS -- history user-relevant changes |
2 Isabelle NEWS -- history user-relevant changes |
2 ============================================== |
3 ============================================== |
3 |
4 |
4 *** Overview of INCOMPATIBILITIES *** |
5 *** Overview of INCOMPATIBILITIES *** |
5 |
6 |
6 * HOL: induct renamed to lfp_induct; |
7 * HOL: induct renamed to lfp_induct; |
|
8 |
|
9 |
|
10 *** Document preparation *** |
|
11 |
|
12 * improved isabelle style files; more abstract symbol implementation |
|
13 (should now use \isamath{...} and \isatext{...} in custom symbol |
|
14 definitions); |
|
15 |
|
16 |
|
17 *** HOL *** |
|
18 |
|
19 * HOL/Library: a collection of generic theories to be used together |
|
20 with main HOL; the theory loader path already includes this directory |
|
21 by default; the following existing theories have been moved here: |
|
22 HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While |
|
23 (as While_Combinator); |
7 |
24 |
8 |
25 |
9 New in Isabelle99-1 (October 2000) |
26 New in Isabelle99-1 (October 2000) |
10 ---------------------------------- |
27 ---------------------------------- |
11 |
28 |