equal
deleted
inserted
replaced
46 end |
46 end |
47 |
47 |
48 * Command 'unbundle' is like 'include', but works within a local theory |
48 * Command 'unbundle' is like 'include', but works within a local theory |
49 context. Unlike "context includes ... begin", the effect of 'unbundle' |
49 context. Unlike "context includes ... begin", the effect of 'unbundle' |
50 on the target context persists, until different declarations are given. |
50 on the target context persists, until different declarations are given. |
|
51 |
|
52 * Proof method "blast" is more robust wrt. corner cases of Pure |
|
53 statements without object-logic judgment. |
51 |
54 |
52 |
55 |
53 *** Prover IDE -- Isabelle/Scala/jEdit *** |
56 *** Prover IDE -- Isabelle/Scala/jEdit *** |
54 |
57 |
55 * Cartouche abbreviations work both for " and ` to accomodate typical |
58 * Cartouche abbreviations work both for " and ` to accomodate typical |
81 established at the end of a proof are properly identified in the theorem |
84 established at the end of a proof are properly identified in the theorem |
82 statement. |
85 statement. |
83 |
86 |
84 |
87 |
85 *** Isar *** |
88 *** Isar *** |
|
89 |
|
90 * The defining position of a literal fact \<open>prop\<close> is maintained more |
|
91 carefully, and made accessible as hyperlink in the Prover IDE. |
|
92 |
|
93 * Commands 'finally' and 'ultimately' used to expose the result as |
|
94 literal fact: this accidental behaviour has been discontinued. Rare |
|
95 INCOMPATIBILITY, use more explicit means to refer to facts in Isar. |
86 |
96 |
87 * Command 'axiomatization' has become more restrictive to correspond |
97 * Command 'axiomatization' has become more restrictive to correspond |
88 better to internal axioms as singleton facts with mandatory name. Minor |
98 better to internal axioms as singleton facts with mandatory name. Minor |
89 INCOMPATIBILITY. |
99 INCOMPATIBILITY. |
90 |
100 |