1 Isabelle NEWS -- history user-relevant changes |
1 Isabelle NEWS -- history user-relevant changes |
2 ============================================== |
2 ============================================== |
3 |
3 |
4 New |
4 New in this Isabelle version |
5 --- |
5 ---------------------------- |
6 |
6 |
7 *** Pure *** |
7 *** Pure *** |
8 |
8 |
9 * 'instance': attached definitions now longer accepted. INCOMPATIBILITY. |
9 * Command 'instance': attached definitions now longer accepted. |
|
10 INCOMPATIBILITY. |
10 |
11 |
11 * Keyword 'code_exception' now named 'code_abort'. INCOMPATIBILITY. |
12 * Keyword 'code_exception' now named 'code_abort'. INCOMPATIBILITY. |
12 |
13 |
13 |
14 |
14 *** HOL *** |
15 *** HOL *** |
15 |
16 |
16 * 'rep_datatype': instead of theorem names the command now takes a list of terms |
17 * Methods "case_tac" and "induct_tac" now refer to the very same rule |
17 denoting the constructors of the type to be represented as datatype. The |
18 declarations as the structured Isar versions "cases" and "induct", cf. |
18 characteristic theorems have to be proven. INCOMPATIBILITY. Also observe that |
19 the corresponding "cases" and "induct" attributes. INCOMPATIBILITY, |
19 the following theorems have disappeared in favour of existing ones: |
20 in rare situations a different rule is selected --- notably nested |
|
21 tuple elimination instead of former prod.exhaust: use explicit |
|
22 (case_tac t rule: prod.exhaust) here. |
|
23 |
|
24 * Removed fact "case_split_thm", which duplicates "case_split". |
|
25 |
|
26 * Command 'rep_datatype': instead of theorem names the command now |
|
27 takes a list of terms denoting the constructors of the type to be |
|
28 represented as datatype. The characteristic theorems have to be |
|
29 proven. INCOMPATIBILITY. Also observe that the following theorems |
|
30 have disappeared in favour of existing ones: |
|
31 |
20 unit_induct ~> unit.induct |
32 unit_induct ~> unit.induct |
21 prod_induct ~> prod.induct |
33 prod_induct ~> prod.induct |
22 sum_induct ~> sum.induct |
34 sum_induct ~> sum.induct |
23 Suc_Suc_eq ~> nat.inject |
35 Suc_Suc_eq ~> nat.inject |
24 Suc_not_Zero Zero_not_Suc ~> nat.distinct |
36 Suc_not_Zero Zero_not_Suc ~> nat.distinct |
25 |
37 |
26 * Tactics induct_tac and thm_induct_tac now take explicit context as arguments; |
|
27 type-specific induction rules are identified by the 'induct' attribute rather |
|
28 than querying the datatype package directly. INCOMPATIBILITY. |
|
29 |
|
30 * 'Least' operator now restricted to class 'order' (and subclasses). |
38 * 'Least' operator now restricted to class 'order' (and subclasses). |
31 INCOMPATIBILITY. |
39 INCOMPATIBILITY. |
32 |
40 |
33 * Library/Nat_Infinity: added addition, numeral syntax and more instantiations |
41 * Library/Nat_Infinity: added addition, numeral syntax and more |
34 for algebraic structures. Removed some duplicate theorems. Changes in simp |
42 instantiations for algebraic structures. Removed some duplicate |
35 rules. INCOMPATIBILITY. |
43 theorems. Changes in simp rules. INCOMPATIBILITY. |
36 |
|
37 |
44 |
38 |
45 |
39 New in Isabelle2008 (June 2008) |
46 New in Isabelle2008 (June 2008) |
40 ------------------------------- |
47 ------------------------------- |
41 |
48 |