equal
deleted
inserted
replaced
19 * Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML |
19 * Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML |
20 interface instead. |
20 interface instead. |
21 |
21 |
22 |
22 |
23 *** Pure *** |
23 *** Pure *** |
|
24 |
|
25 * Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm |
|
26 to 'a -> thm, at the cost of internal tagging of results with an |
|
27 authentic oracle name. The Isar command 'oracle' is now polymorphic, |
|
28 no argument type is specified. INCOMPATIBILITY, need to simplify |
|
29 existing oracle code accordingly. Note that extra performance may be |
|
30 gained by producing the cterm carefully, not via Thm.cterm_of. |
24 |
31 |
25 * Changed defaults for unify configuration options: |
32 * Changed defaults for unify configuration options: |
26 |
33 |
27 unify_trace_bound = 50 (formerly 25) |
34 unify_trace_bound = 50 (formerly 25) |
28 unify_search_bound = 60 (formerly 30) |
35 unify_search_bound = 60 (formerly 30) |