equal
deleted
inserted
replaced
13 "timeout_scale" --- this already used for the overall session build |
13 "timeout_scale" --- this already used for the overall session build |
14 process before, and allows to adapt to slow machines. The underlying |
14 process before, and allows to adapt to slow machines. The underlying |
15 Timeout.apply in Isabelle/ML treats an original timeout specification 0 |
15 Timeout.apply in Isabelle/ML treats an original timeout specification 0 |
16 as no timeout; before it meant immediate timeout. Rare INCOMPATIBILITY |
16 as no timeout; before it meant immediate timeout. Rare INCOMPATIBILITY |
17 in boundary cases. |
17 in boundary cases. |
|
18 |
|
19 |
|
20 *** Document preparation *** |
|
21 |
|
22 * More accurate LaTeX typesetting of \<open>...\<close> using \guilsinglleft ... |
|
23 \guilsinglright. Minor INCOMPATIBILITY, use \usepackage[T1]{fontenc} |
|
24 (which is now also the default in "isabelle mkroot"). |
18 |
25 |
19 |
26 |
20 *** HOL *** |
27 *** HOL *** |
21 |
28 |
22 * Theory Multiset: dedicated predicate "multiset" is gone, use |
29 * Theory Multiset: dedicated predicate "multiset" is gone, use |