40 expression m consecutively to each subgoal, constructing individual |
40 expression m consecutively to each subgoal, constructing individual |
41 subproofs internally. This impacts the internal construction of proof |
41 subproofs internally. This impacts the internal construction of proof |
42 terms: it makes a cascade of let-expressions within the derivation tree |
42 terms: it makes a cascade of let-expressions within the derivation tree |
43 and may thus improve scalability. |
43 and may thus improve scalability. |
44 |
44 |
45 * New attribute "trace_locales" for tracing activation of locale |
45 * Attribute "trace_locales" activates tracing of locale instances during |
46 instances during roundup. It replaces the diagnostic command |
46 roundup. It replaces the diagnostic command 'print_dependencies', which |
47 'print_dependencies', which was removed. |
47 has been discontinued. |
48 |
48 |
49 |
49 |
50 *** Isabelle/jEdit Prover IDE *** |
50 *** Isabelle/jEdit Prover IDE *** |
51 |
51 |
52 * Prover IDE startup is now much faster, because theory dependencies are |
52 * Prover IDE startup is now much faster, because theory dependencies are |
57 sufficient and more convenient to start editing a particular session. |
57 sufficient and more convenient to start editing a particular session. |
58 |
58 |
59 |
59 |
60 *** HOL *** |
60 *** HOL *** |
61 |
61 |
62 * Improvements of the "lift_bnf" command: |
62 * Improvements of the 'lift_bnf' command: |
63 - Add support for quotient types. |
63 - Add support for quotient types. |
64 - Generate transfer rules for the lifted map/set/rel/pred |
64 - Generate transfer rules for the lifted map/set/rel/pred constants |
65 constants (theorems "<type>.<constant>_transfer_raw"). |
65 (theorems "<type>.<constant>_transfer_raw"). |
66 |
66 |
67 * Term_XML.Encode/Decode.term uses compact representation of Const |
67 * Term_XML.Encode/Decode.term uses compact representation of Const |
68 "typargs" from the given declaration environment. This also makes more |
68 "typargs" from the given declaration environment. This also makes more |
69 sense for translations to lambda-calculi with explicit polymorphism. |
69 sense for translations to lambda-calculi with explicit polymorphism. |
70 INCOMPATIBILITY, use Term_XML.Encode/Decode.term_raw in special |
70 INCOMPATIBILITY, use Term_XML.Encode/Decode.term_raw in special |
71 applications. |
71 applications. |
72 |
72 |
73 * ASCII membership syntax concerning big operators for infimum and |
73 * ASCII membership syntax concerning big operators for infimum and |
74 supremum is gone. INCOMPATIBILITY. |
74 supremum has been discontinued. INCOMPATIBILITY. |
75 |
75 |
76 * Clear distinction between types for bits (False / True) and Z2 (0 / |
76 * Clear distinction between types for bits (False / True) and Z2 (0 / |
77 1): theory HOL/Library/Bit.thy has been renamed accordingly. |
77 1): theory HOL-Library.Bit has been renamed accordingly. |
78 INCOMPATIBILITY. |
78 INCOMPATIBILITY. |
79 |
79 |
80 * Fact collections algebra_split_simps and field_split_simps correspond |
80 * Dynamic facts "algebra_split_simps" and "field_split_simps" correspond |
81 to algebra_simps and field_simps but contain more aggressive rules |
81 to algebra_simps and field_simps but contain more aggressive rules |
82 potentially splitting goals; algebra_split_simps roughly replaces |
82 potentially splitting goals; algebra_split_simps roughly replaces |
83 sign_simps and field_split_simps can be used instead of divide_simps. |
83 sign_simps and field_split_simps can be used instead of divide_simps. |
84 INCOMPATIBILITY. |
84 INCOMPATIBILITY. |
85 |
85 |