equal
deleted
inserted
replaced
32 is called fastforce / fast_force_tac already since Isabelle2011-1. |
32 is called fastforce / fast_force_tac already since Isabelle2011-1. |
33 |
33 |
34 * Updated and extended "isar-ref" and "implementation" manual, reduced |
34 * Updated and extended "isar-ref" and "implementation" manual, reduced |
35 remaining material in old "ref" manual. |
35 remaining material in old "ref" manual. |
36 |
36 |
37 * Improved support for auxiliary contexts indicate block structure for |
37 * Improved support for auxiliary contexts that indicate block structure |
38 specifications: nesting of "context fixes ... context assumes ..." |
38 for specifications. Nesting of "context fixes ... context assumes ..." |
39 and "class ... context ...". |
39 and "class ... context ...". |
40 |
40 |
41 * Attribute "consumes" allows a negative value as well, which is |
41 * Attribute "consumes" allows a negative value as well, which is |
42 interpreted relatively to the total number of premises of the rule in |
42 interpreted relatively to the total number of premises of the rule in |
43 the target context. This form of declaration is stable when exported |
43 the target context. This form of declaration is stable when exported |
283 less_eq_list.drop ~> less_eq_list_drop |
283 less_eq_list.drop ~> less_eq_list_drop |
284 less_eq_list.induct ~> less_eq_list_induct |
284 less_eq_list.induct ~> less_eq_list_induct |
285 not_le_list_length ~> Sublist.not_sublisteq_length |
285 not_le_list_length ~> Sublist.not_sublisteq_length |
286 |
286 |
287 INCOMPATIBILITY. |
287 INCOMPATIBILITY. |
288 |
|
289 |
288 |
290 * New theory Library/Countable_Set. |
289 * New theory Library/Countable_Set. |
291 |
290 |
292 * Theory Library/Debug and Library/Parallel provide debugging and |
291 * Theory Library/Debug and Library/Parallel provide debugging and |
293 parallel execution for code generated towards Isabelle/ML. |
292 parallel execution for code generated towards Isabelle/ML. |