38 * HOL/ML: even fewer consts are declared as global (see theories Ord, |
38 * HOL/ML: even fewer consts are declared as global (see theories Ord, |
39 Lfp, Gfp, WF); this only affects ML packages that refer to const names |
39 Lfp, Gfp, WF); this only affects ML packages that refer to const names |
40 internally; |
40 internally; |
41 |
41 |
42 * Isar: changed syntax of local blocks from {{ }} to { }; |
42 * Isar: changed syntax of local blocks from {{ }} to { }; |
|
43 |
|
44 * FOL, ZF: AddIffs now available, giving theorems of the form P<->Q to the |
|
45 simplifier and classical reasoner simultaneously; |
43 |
46 |
44 * Provers: Blast_tac now warns of and ignores "weak elimination rules" e.g. |
47 * Provers: Blast_tac now warns of and ignores "weak elimination rules" e.g. |
45 [| inj ?f; ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W |
48 [| inj ?f; ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W |
46 use instead the strong form, |
49 use instead the strong form, |
47 [| inj ?f; ~ ?W ==> ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W |
50 [| inj ?f; ~ ?W ==> ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W |
48 In HOL, FOL and ZF the function cla_make_elim will create such rules |
51 In HOL, FOL and ZF the function cla_make_elim will create such rules |
49 from destruct-rules. |
52 from destruct-rules; |
50 |
53 |
51 * ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global |
54 * ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global |
52 timing flag supersedes proof_timing and Toplevel.trace; |
55 timing flag supersedes proof_timing and Toplevel.trace; |
53 |
56 |
54 * ML: PureThy.add_thms/add_axioms/add_defs return theorems as well; |
57 * ML: PureThy.add_thms/add_axioms/add_defs return theorems as well; |