equal
deleted
inserted
replaced
4 (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.) |
4 (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.) |
5 |
5 |
6 |
6 |
7 New in this Isabelle version |
7 New in this Isabelle version |
8 ---------------------------- |
8 ---------------------------- |
|
9 |
|
10 *** General *** |
|
11 |
|
12 * Timeouts for Isabelle/ML tools are subject to system option |
|
13 "timeout_scale" --- this already used for the overall session build |
|
14 process before, and allows to adapt to slow machines. The underlying |
|
15 Timeout.apply in Isabelle/ML treats an original timeout specification 0 |
|
16 as no timeout; before it meant immediate timeout. Rare INCOMPATIBILITY |
|
17 in boundary cases. |
|
18 |
9 |
19 |
10 *** HOL *** |
20 *** HOL *** |
11 |
21 |
12 * Theory Multiset: dedicated predicate "multiset" is gone, use |
22 * Theory Multiset: dedicated predicate "multiset" is gone, use |
13 explict expression instead. Minor INCOMPATIBILITY. |
23 explict expression instead. Minor INCOMPATIBILITY. |