equal
deleted
inserted
replaced
39 syntax just like the Isar command 'by'. |
39 syntax just like the Isar command 'by'. |
40 |
40 |
41 |
41 |
42 *** HOL *** |
42 *** HOL *** |
43 |
43 |
44 * HOL-Rational: 'Fract k 0' now equals '0'. INCOMPATIBILITY. |
44 * HOL/Library/GCD: Curried operations gcd, lcm (for nat) and zgcd, zlcm (for int); |
|
45 carried together from various gcd/lcm developements in the HOL Distribution. |
|
46 zgcd and zlcm replace former igcd and ilcm; corresponding theorems renamed |
|
47 accordingly. INCOMPATIBILY. To recover tupled syntax, use syntax declarations like: |
|
48 |
|
49 hide (open) const gcd |
|
50 abbreviation gcd where |
|
51 "gcd == (%(a, b). GCD.gcd a b)" |
|
52 notation (output) |
|
53 GCD.gcd ("gcd '(_, _')") |
|
54 |
|
55 (analogously for lcm, zgcd, zlcm). |
|
56 |
|
57 * HOL/Real/Rational: 'Fract k 0' now equals '0'. INCOMPATIBILITY. |
45 |
58 |
46 * Integrated image HOL-Complex with HOL. Entry points Main.thy and |
59 * Integrated image HOL-Complex with HOL. Entry points Main.thy and |
47 Complex_Main.thy remain as they are. |
60 Complex_Main.thy remain as they are. |
48 |
61 |
49 * New image HOL-Plain provides a minimal HOL with the most important tools |
62 * New image HOL-Plain provides a minimal HOL with the most important tools |