equal
deleted
inserted
replaced
52 * Session Pure-Examples contains notable examples for Isabelle/Pure |
52 * Session Pure-Examples contains notable examples for Isabelle/Pure |
53 (former entries of HOL-Isar_Examples). |
53 (former entries of HOL-Isar_Examples). |
54 |
54 |
55 * Definitions in locales produce rule which can be added as congruence |
55 * Definitions in locales produce rule which can be added as congruence |
56 rule to protect foundational terms during simplification. |
56 rule to protect foundational terms during simplification. |
|
57 |
|
58 * Consolidated terminology and function signatures for nested targets: |
|
59 |
|
60 * Local_Theory.begin_nested replaces Local_Theory.open_target. |
|
61 |
|
62 * Local_Theory.end_nested replaces Local_Theory.close_target. |
|
63 |
|
64 INCOMPATIBILITY. |
57 |
65 |
58 |
66 |
59 *** HOL *** |
67 *** HOL *** |
60 |
68 |
61 * Nitpick/Kodkod may be invoked directly within the running |
69 * Nitpick/Kodkod may be invoked directly within the running |