
1 
1 Isabelle NEWS  history userrelevant changes 
2 Isabelle NEWS  history userrelevant changes 
2 ============================================== 
3 ============================================== 
3 
4 
4 New in this Isabelle version 
5 New in this Isabelle version 
5  
6  
6 
7 
7 *** Overview of INCOMPATIBILITIES (see below for more details) *** 
8 *** Overview of INCOMPATIBILITIES (see below for more details) *** 
8 
9 
9 * HOL: the constant for f``x is now "image" rather than "op ``". 
10 * HOL: the constant for f``x is now "image" rather than "op ``"; 
10 
11 
11 * HOL: the cartesian product is now "<*>" instead of "Times". 
12 * HOL: the cartesian product is now "<*>" instead of "Times"; the 
12 the lexicographic product is now "<*lex*>" instead of "**". 
13 lexicographic product is now "<*lex*>" instead of "**"; 
13 
14 
14 * HOL: exhaust_tac on datatypes superceded by new generic case_tac; 
15 * HOL: exhaust_tac on datatypes superceded by new generic case_tac; 
15 
16 
16 * HOL: simplification no longer dives into caseexpressions 
17 * HOL: simplification no longer dives into caseexpressions 
17 
18 
18 * HOL: the recursion equations generated by 'recdef' are now called 
19 * HOL: the recursion equations generated by 'recdef' are now called 
19 f.simps instead of f.rules; 
20 f.simps instead of f.rules; 
20 
21 
21 * ML: PureThy.add_thms/add_axioms/add_defs return theorems as well; 
22 * ML: PureThy.add_thms/add_axioms/add_defs return theorems as well; 

23 

24 * LaTeX: several improvements of isabelle.sty; 
22 
25 
23 
26 
24 *** Document preparation *** 
27 *** Document preparation *** 
25 
28 
26 * isatool mkdir provides easy setup of Isabelle session directories, 
29 * isatool mkdir provides easy setup of Isabelle session directories, 
85 * simplified (more robust) goal selection of proof methods: 1st goal, 
88 * simplified (more robust) goal selection of proof methods: 1st goal, 
86 all goals, or explicit goal specifier (tactic emulation); thus 'proof 
89 all goals, or explicit goal specifier (tactic emulation); thus 'proof 
87 method scripts' have to be in depthfirst order; 
90 method scripts' have to be in depthfirst order; 
88 
91 
89 * tuned 'let' syntax: replace 'as' keyword by 'and'; 
92 * tuned 'let' syntax: replace 'as' keyword by 'and'; 

93 

94 * theory command 'hide' removes declarations from class/type/const 

95 name spaces; 
90 
96 
91 
97 
92 *** HOL *** 
98 *** HOL *** 
93 
99 
94 * HOL/Algebra: new theory of rings and univariate polynomials, by 
100 * HOL/Algebra: new theory of rings and univariate polynomials, by 
121 resulting in a separate list of theorems for each equation; 
127 resulting in a separate list of theorems for each equation; 
122 
128 
123 
129 
124 *** General *** 
130 *** General *** 
125 
131 

132 * improved name spaces: ambiguous output is qualified; support for 

133 hiding of names; 

134 
126 * compression of ML heaps images may now be controlled via c option 
135 * compression of ML heaps images may now be controlled via c option 
127 of isabelle and isatool usedir (currently only observed by Poly/ML); 
136 of isabelle and isatool usedir (currently only observed by Poly/ML); 
128 
137 
129 * ML: new combinators >> and >>> for incremental transformations 
138 * ML: new combinators >> and >>> for incremental transformations 
130 with secondary results (e.g. certain theory extensions): 
139 with secondary results (e.g. certain theory extensions): 
161 uses the default simpset instead of a supplied list of theorems. 
170 uses the default simpset instead of a supplied list of theorems. 
162 
171 
163 * HOL/List: the constructors of type list are now Nil and Cons; 
172 * HOL/List: the constructors of type list are now Nil and Cons; 
164 
173 
165 * Simplifier: the type of the infix ML functions 
174 * Simplifier: the type of the infix ML functions 
166 setSSolver addSSolver setSolver addSolver 
175 setSSolver addSSolver setSolver addSolver 
167 is now simpset * solver > simpset where `solver' is a new abstract type 
176 is now simpset * solver > simpset where `solver' is a new abstract type 
168 for packaging solvers. A solver is created via 
177 for packaging solvers. A solver is created via 
169 mk_solver: string > (thm list > int > tactic) > solver 
178 mk_solver: string > (thm list > int > tactic) > solver 
170 where the string argument is only a comment. 
179 where the string argument is only a comment. 
171 
180 
172 
181 
173 *** Proof tools *** 
182 *** Proof tools *** 
174 
183 