equal
deleted
inserted
replaced
38 position information via constraints). |
38 position information via constraints). |
39 |
39 |
40 * Simplified configuration options for syntax ambiguity: see |
40 * Simplified configuration options for syntax ambiguity: see |
41 "syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref |
41 "syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref |
42 manual. Minor INCOMPATIBILITY. |
42 manual. Minor INCOMPATIBILITY. |
|
43 |
|
44 * Forward declaration of outer syntax keywords within the theory |
|
45 header -- minor INCOMPATIBILITY for user-defined commands. Allow new |
|
46 commands to be used in the same theory where defined. |
43 |
47 |
44 |
48 |
45 *** Pure *** |
49 *** Pure *** |
46 |
50 |
47 * Attribute "abs_def" turns an equation of the form "f x y == t" into |
51 * Attribute "abs_def" turns an equation of the form "f x y == t" into |
369 |
373 |
370 * New "case_product" attribute (see HOL). |
374 * New "case_product" attribute (see HOL). |
371 |
375 |
372 |
376 |
373 *** ML *** |
377 *** ML *** |
374 |
|
375 * Outer syntax keywords for user-defined Isar commands need to be |
|
376 defined explicitly in the theory header. Minor INCOMPATIBILITY. |
|
377 |
378 |
378 * Antiquotation @{keyword "name"} produces a parser for outer syntax |
379 * Antiquotation @{keyword "name"} produces a parser for outer syntax |
379 from a minor keyword introduced via theory header declaration. |
380 from a minor keyword introduced via theory header declaration. |
380 |
381 |
381 * Local_Theory.define no longer hard-wires default theorem name |
382 * Local_Theory.define no longer hard-wires default theorem name |