equal
deleted
inserted
replaced
33 simplification rules whose lhs match term. Any other term is |
33 simplification rules whose lhs match term. Any other term is |
34 interpreted as pattern and selects all theorems matching the |
34 interpreted as pattern and selects all theorems matching the |
35 pattern. Available in ProofGeneral under 'ProofGeneral -> Find |
35 pattern. Available in ProofGeneral under 'ProofGeneral -> Find |
36 Theorems' or C-c C-f. Example: |
36 Theorems' or C-c C-f. Example: |
37 |
37 |
38 C-c C-f (100) "(_::nat) + _ + _" intro -name:"HOL." |
38 C-c C-f (100) "(_::nat) + _ + _" intro -name: "HOL." |
39 |
39 |
40 prints the last 100 theorems matching the pattern "(_::nat) + _ + _", |
40 prints the last 100 theorems matching the pattern "(_::nat) + _ + _", |
41 matching the current goal as introduction rule and not having "HOL." |
41 matching the current goal as introduction rule and not having "HOL." |
42 in their name (i.e. not being defined in theory HOL). |
42 in their name (i.e. not being defined in theory HOL). |
43 |
43 |
147 ML expression of type theory -> T -> term into a primitive rule of |
147 ML expression of type theory -> T -> term into a primitive rule of |
148 type theory -> T -> thm (i.e. the functionality of Thm.invoke_oracle |
148 type theory -> T -> thm (i.e. the functionality of Thm.invoke_oracle |
149 is already included here); see also FOL/ex/IffExample.thy; |
149 is already included here); see also FOL/ex/IffExample.thy; |
150 INCOMPATIBILITY. |
150 INCOMPATIBILITY. |
151 |
151 |
|
152 * axclass: name space prefix for class "c" is now "c_class" (was "c" |
|
153 before); "cI" is no longer bound, use "c.intro" instead. |
|
154 INCOMPATIBILITY. This change avoids clashes of fact bindings for |
|
155 axclasses vs. locales. |
|
156 |
152 * Improved internal renaming of symbolic identifiers -- attach primes |
157 * Improved internal renaming of symbolic identifiers -- attach primes |
153 instead of base 26 numbers. |
158 instead of base 26 numbers. |
154 |
159 |
155 * New flag show_question_marks controls printing of leading question |
160 * New flag show_question_marks controls printing of leading question |
156 marks in schematic variable names. |
161 marks in schematic variable names. |
207 use isatool fixcpure to adapt your theory and ML sources. |
212 use isatool fixcpure to adapt your theory and ML sources. |
208 |
213 |
209 * New syntax 'name(i-j, i-, i, ...)' for referring to specific |
214 * New syntax 'name(i-j, i-, i, ...)' for referring to specific |
210 selections of theorems in named facts via index ranges. |
215 selections of theorems in named facts via index ranges. |
211 |
216 |
212 * More efficient treatment of intermediate checkpoints in interactive |
|
213 theory development. |
|
214 |
|
215 * 'print_theorems': in theory mode, really print the difference |
217 * 'print_theorems': in theory mode, really print the difference |
216 wrt. the last state (works for interactive theory development only), |
218 wrt. the last state (works for interactive theory development only), |
217 in proof mode print all local facts (cf. 'print_facts'); |
219 in proof mode print all local facts (cf. 'print_facts'); |
|
220 |
|
221 * More efficient treatment of intermediate checkpoints in interactive |
|
222 theory development. |
218 |
223 |
219 |
224 |
220 *** Locales *** |
225 *** Locales *** |
221 |
226 |
222 * New commands for the interpretation of locale expressions in theories (1), |
227 * New commands for the interpretation of locale expressions in theories (1), |
374 |
379 |
375 New simproc record_upd_simproc for simplification of multiple record |
380 New simproc record_upd_simproc for simplification of multiple record |
376 updates enabled by default. Moreover, trivial updates are also |
381 updates enabled by default. Moreover, trivial updates are also |
377 removed: r(|x := x r|) = r. INCOMPATIBILITY: old proofs break |
382 removed: r(|x := x r|) = r. INCOMPATIBILITY: old proofs break |
378 occasionally, since simplification is more powerful by default. |
383 occasionally, since simplification is more powerful by default. |
|
384 |
|
385 * typedef: proper support for polymorphic sets, which contain extra |
|
386 type-variables in the term. |
379 |
387 |
380 * Simplifier: automatically reasons about transitivity chains |
388 * Simplifier: automatically reasons about transitivity chains |
381 involving "trancl" (r^+) and "rtrancl" (r^*) by setting up tactics |
389 involving "trancl" (r^+) and "rtrancl" (r^*) by setting up tactics |
382 provided by Provers/trancl.ML as additional solvers. INCOMPATIBILITY: |
390 provided by Provers/trancl.ML as additional solvers. INCOMPATIBILITY: |
383 old proofs break occasionally as simplification may now solve more |
391 old proofs break occasionally as simplification may now solve more |