equal
deleted
inserted
replaced
6 |
6 |
7 *** General *** |
7 *** General *** |
8 |
8 |
9 * Commands 'method_setup' and 'attribute_setup' now work within a |
9 * Commands 'method_setup' and 'attribute_setup' now work within a |
10 local theory context. |
10 local theory context. |
|
11 |
|
12 * Command 'named_theorems' declares a dynamic fact within the context, |
|
13 together with an attribute to maintain the content incrementally. |
|
14 This supersedes functor Named_Thms, but with a subtle change of |
|
15 semantics due to external visual order vs. internal reverse order. |
11 |
16 |
12 |
17 |
13 *** HOL *** |
18 *** HOL *** |
14 |
19 |
15 * Sledgehammer: |
20 * Sledgehammer: |