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 Cc Cf. Example: 
36 Theorems' or Cc Cf. Example: 
37 
37 
38 Cc Cf (100) "(_::nat) + _ + _" intro name:"HOL." 
38 Cc Cf (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(ij, i, i, ...)' for referring to specific 
214 * New syntax 'name(ij, 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 typevariables 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 