equal
deleted
inserted
replaced
3 |
3 |
4 New in this Isabelle release |
4 New in this Isabelle release |
5 ---------------------------- |
5 ---------------------------- |
6 |
6 |
7 *** General *** |
7 *** General *** |
|
8 |
|
9 * The type Library.option is no more, along with the exception |
|
10 Library.OPTION: Isabelle now uses the standard option type. The |
|
11 functions the, is_some, is_none, etc. are still in Library, but |
|
12 the constructors are now SOME and NONE instead of Some and None. |
8 |
13 |
9 * Document preparation: new antiquotations @{lhs thm} and @{rhs thm} |
14 * Document preparation: new antiquotations @{lhs thm} and @{rhs thm} |
10 printing the lhs/rhs of definitions, equations, inequations etc. |
15 printing the lhs/rhs of definitions, equations, inequations etc. |
11 |
16 |
12 * isatool usedir: new option -f that allows specification of the ML |
17 * isatool usedir: new option -f that allows specification of the ML |