equal
deleted
inserted
replaced
27 |
27 |
28 * Provers: improved induct method: assumptions introduced by case |
28 * Provers: improved induct method: assumptions introduced by case |
29 "foo" are split into "foo.hyps" (from the rule) and "foo.prems" (from |
29 "foo" are split into "foo.hyps" (from the rule) and "foo.prems" (from |
30 the goal statement); "foo" still refers to all facts collectively; |
30 the goal statement); "foo" still refers to all facts collectively; |
31 |
31 |
32 * Provers: Simplifier.simproc(_i) now provide sane interface for |
|
33 setting up simprocs; |
|
34 |
|
35 |
32 |
36 *** HOL *** |
33 *** HOL *** |
37 |
34 |
38 * 'typedef' command has new option "open" to suppress the set |
35 * 'typedef' command has new option "open" to suppress the set |
39 definition; |
36 definition; |
50 |
47 |
51 "n div 2 + (n+1) div 2 = (n::nat)" |
48 "n div 2 + (n+1) div 2 = (n::nat)" |
52 |
49 |
53 * simp's arithmetic capabilities have been enhanced a bit: it now |
50 * simp's arithmetic capabilities have been enhanced a bit: it now |
54 takes ~= in premises into account (by performing a case split); |
51 takes ~= in premises into account (by performing a case split); |
|
52 |
|
53 |
|
54 *** ML *** |
|
55 |
|
56 * Pure: Tactic.prove provides sane interface for internal proofs; |
|
57 omits the infamous "standard" operation, so this is more appropriate |
|
58 than prove_goalw_cterm in many situations (e.g. in simprocs); |
|
59 |
|
60 * Pure: improved error reporting of simprocs; |
|
61 |
|
62 * Provers: Simplifier.simproc(_i) provides sane interface for setting |
|
63 up simprocs; |
55 |
64 |
56 |
65 |
57 |
66 |
58 New in Isabelle2002 (March 2002) |
67 New in Isabelle2002 (March 2002) |
59 -------------------------------- |
68 -------------------------------- |