equal
deleted
inserted
replaced
147 * directory HOL/Real: a construction of the reals using Dedekind cuts |
147 * directory HOL/Real: a construction of the reals using Dedekind cuts |
148 (not included by default); |
148 (not included by default); |
149 |
149 |
150 * directory HOL/UNITY: Chandy and Misra's UNITY formalism; |
150 * directory HOL/UNITY: Chandy and Misra's UNITY formalism; |
151 |
151 |
|
152 * calling (stac rew i) now fails if "rew" has no effect on the goal |
|
153 [previously, this check worked only if the rewrite rule was unconditional] |
|
154 |
152 |
155 |
153 *** ZF *** |
156 *** ZF *** |
154 |
157 |
155 * in let x=t in u(x), neither t nor u(x) has to be an FOL term. |
158 * in let x=t in u(x), neither t nor u(x) has to be an FOL term. |
|
159 |
|
160 * calling (stac rew i) now fails if "rew" has no effect on the goal |
|
161 [previously, this check worked only if the rewrite rule was unconditional] |
156 |
162 |
157 |
163 |
158 *** Internal programming interfaces *** |
164 *** Internal programming interfaces *** |
159 |
165 |
160 * improved the theory data mechanism to support encapsulation (data |
166 * improved the theory data mechanism to support encapsulation (data |
167 * Simplifier now offers conversions (asm_)(full_)rewrite: simpset -> |
173 * Simplifier now offers conversions (asm_)(full_)rewrite: simpset -> |
168 cterm -> thm; |
174 cterm -> thm; |
169 |
175 |
170 * Pure: several new basic modules made available for general use, see |
176 * Pure: several new basic modules made available for general use, see |
171 also src/Pure/README; |
177 also src/Pure/README; |
|
178 |
|
179 * new tactical CHANGED_GOAL for checking that a tactic modifies a subgoal |
172 |
180 |
173 |
181 |
174 |
182 |
175 New in Isabelle98 (January 1998) |
183 New in Isabelle98 (January 1998) |
176 -------------------------------- |
184 -------------------------------- |