equal
deleted
inserted
replaced
|
1 |
1 Isabelle NEWS -- history user-relevant changes |
2 Isabelle NEWS -- history user-relevant changes |
2 ============================================== |
3 ============================================== |
3 |
4 |
4 New in this Isabelle release |
5 New in this Isabelle release |
5 ---------------------------- |
6 ---------------------------- |
6 |
7 |
7 *** General *** |
8 *** General *** |
|
9 |
|
10 * Pure: locale specifications now produce predicate definitions |
|
11 according to the body of text (covering assumptions modulo local |
|
12 definitions); predicate "loc_axioms" covers newly introduced text, |
|
13 while "loc" is cumulative wrt. all included locale expressions; the |
|
14 latter view is presented only on export into the global theory |
|
15 context; potential INCOMPATIBILITY, use "(open)" option to fall back |
|
16 on the old view without predicates; |
8 |
17 |
9 * improved thms_containing: proper indexing of facts instead of raw |
18 * improved thms_containing: proper indexing of facts instead of raw |
10 theorems; check validity of results wrt. current name space; include |
19 theorems; check validity of results wrt. current name space; include |
11 local facts of proof configuration (also covers active locales); an |
20 local facts of proof configuration (also covers active locales); an |
12 optional limit for the number of printed facts may be given (the |
21 optional limit for the number of printed facts may be given (the |