equal
deleted
inserted
replaced
19 |
19 |
20 * Theory loader: use_thy (and similar operations) no longer set the |
20 * Theory loader: use_thy (and similar operations) no longer set the |
21 implicit ML context, which was occasionally hard to predict and in |
21 implicit ML context, which was occasionally hard to predict and in |
22 conflict with concurrency. INCOMPATIBILITY, use ML within Isar which |
22 conflict with concurrency. INCOMPATIBILITY, use ML within Isar which |
23 provides a proper context already. |
23 provides a proper context already. |
|
24 |
|
25 * Theory loader: old-style ML proof scripts being *attached* to a thy |
|
26 file are no longer supported. INCOMPATIBILITY, regular 'uses' and |
|
27 'use' within a theory file will do the job. |
24 |
28 |
25 |
29 |
26 *** Pure *** |
30 *** Pure *** |
27 |
31 |
28 * Instantiation target allows for simultaneous specification of class |
32 * Instantiation target allows for simultaneous specification of class |
42 |
46 |
43 * Theory Nat: renamed less_imp_le to less_imp_le_nat; removed |
47 * Theory Nat: renamed less_imp_le to less_imp_le_nat; removed |
44 redundant lemmas less_trans, less_linear, le_imp_less_or_eq, |
48 redundant lemmas less_trans, less_linear, le_imp_less_or_eq, |
45 le_less_trans, less_le_trans, which merely duplicate lemmas of the |
49 le_less_trans, less_le_trans, which merely duplicate lemmas of the |
46 same name in theory Orderings. Potential INCOMPATIBILITY due to more |
50 same name in theory Orderings. Potential INCOMPATIBILITY due to more |
47 general and different variable names. |
51 general types and different variable names. |
48 |
52 |
49 * Library/Option_ord.thy: Canonical order on option type. |
53 * Library/Option_ord.thy: Canonical order on option type. |
50 |
54 |
51 * Library/RBT.thy: New theory of red-black trees, an efficient |
55 * Library/RBT.thy: New theory of red-black trees, an efficient |
52 implementation of finite maps. |
56 implementation of finite maps. |