equal
deleted
inserted
replaced
25 |
25 |
26 INCOMPATIBILITY. |
26 INCOMPATIBILITY. |
27 |
27 |
28 * Removed simplifier congruence rule of "prod_case", as has for long |
28 * Removed simplifier congruence rule of "prod_case", as has for long |
29 been the case with "split". |
29 been the case with "split". |
|
30 |
|
31 * Datatype package: theorems generated for executable equality |
|
32 (class eq) carry proper names and are treated as default code |
|
33 equations. |
|
34 |
|
35 * List.thy: use various operations from the Haskell prelude when |
|
36 generating Haskell code. |
|
37 |
30 |
38 |
31 |
39 |
32 New in Isabelle2009-2 (June 2010) |
40 New in Isabelle2009-2 (June 2010) |
33 --------------------------------- |
41 --------------------------------- |
34 |
42 |