43 |
43 |
44 * HOL/ML: even fewer consts are declared as global (see theories Ord, |
44 * HOL/ML: even fewer consts are declared as global (see theories Ord, |
45 Lfp, Gfp, WF); this only affects ML packages that refer to const names |
45 Lfp, Gfp, WF); this only affects ML packages that refer to const names |
46 internally; |
46 internally; |
47 |
47 |
48 * HOL, ZF: syntax for quotienting wrt an equivalence relation changed from |
48 * HOL, ZF: syntax for quotienting wrt an equivalence relation changed |
49 A/r to A//r; |
49 from A/r to A//r; |
|
50 |
|
51 * HOL: qed_spec_mp now also removes bounded ALL; |
50 |
52 |
51 * ZF: new treatment of arithmetic (nat & int) may break some old proofs; |
53 * ZF: new treatment of arithmetic (nat & int) may break some old proofs; |
52 |
54 |
53 * Isar/Provers: intro/elim/dest attributes: changed |
55 * Isar/Provers: intro/elim/dest attributes: changed |
54 intro/intro!/intro!! flags to intro!/intro/intro? (in most cases, one |
56 intro/intro!/intro!! flags to intro!/intro/intro? (in most cases, one |
55 should have to change intro!! to intro? only); |
57 should have to change intro!! to intro? only); |
56 |
58 |
57 * Isar: changed syntax of local blocks from {{ }} to { }; |
59 * Isar: changed syntax of local blocks from {{ }} to { }; |
58 |
60 |
59 * Isar: renamed 'RS' attribute to 'THEN'; |
61 * Isar: renamed 'RS' attribute to 'THEN'; |
|
62 |
|
63 * Isar: renamed some attributes (rulify -> rulified, elimify -> elimified, ...); |
60 |
64 |
61 * Isar/HOL: renamed "intrs" to "intros" in inductive definitions; |
65 * Isar/HOL: renamed "intrs" to "intros" in inductive definitions; |
62 |
66 |
63 * Provers: strengthened force_tac by using new first_best_tac; |
67 * Provers: strengthened force_tac by using new first_best_tac; |
64 |
68 |
291 |
295 |
292 * new tactic induct_thm_tac: thm -> string -> int -> tactic |
296 * new tactic induct_thm_tac: thm -> string -> int -> tactic |
293 induct_tac th "x1 ... xn" expects th to have a conclusion of the form |
297 induct_tac th "x1 ... xn" expects th to have a conclusion of the form |
294 P v1 ... vn and abbreviates res_inst_tac [("v1","x1"),...,("vn","xn")] th; |
298 P v1 ... vn and abbreviates res_inst_tac [("v1","x1"),...,("vn","xn")] th; |
295 |
299 |
296 * new function rulify: thm -> thm for turning outer -->/! into ==>/?; |
300 * new functions rulify/rulify_no_asm: thm -> thm for turning outer |
297 behaves like qed_spec_mp; |
301 -->/All/Ball into ==>/!!; qed_spec_mp now uses rulify_no_asm; |
298 |
302 |
299 * theory Sexp now in HOL/Induct examples (it used to be part of main |
303 * theory Sexp now in HOL/Induct examples (it used to be part of main |
300 HOL, but was unused); |
304 HOL, but was unused); |
301 |
305 |
302 * fewer consts declared as global (e.g. have to refer to "Lfp.lfp" |
306 * fewer consts declared as global (e.g. have to refer to "Lfp.lfp" |