30 * HOL: 'inductive' now longer features separate (collective) |
30 * HOL: 'inductive' now longer features separate (collective) |
31 attributes for 'intros'; |
31 attributes for 'intros'; |
32 |
32 |
33 |
33 |
34 *** HOL *** |
34 *** HOL *** |
|
35 |
|
36 * HOL: moved over to sane numeral syntax; the new policy is as |
|
37 follows: |
|
38 |
|
39 - 0 and 1 are polymorphic constants, which are defined on any |
|
40 numeric type (nat, int, real etc.); |
|
41 |
|
42 - 2, 3, 4, ... and -1, -2, -3, ... are polymorphic numerals, based |
|
43 binary representation internally; |
|
44 |
|
45 - type nat has special constructor Suc, and generally prefers Suc 0 |
|
46 over 1::nat and Suc (Suc 0) over 2::nat; |
|
47 |
|
48 This change may cause significant INCOMPATIBILITIES; here are some |
|
49 hints on converting existing sources: |
|
50 |
|
51 - due to the new "num" token, "-0" and "-1" etc. are now atomic |
|
52 entities, so expressions involving "-" (unary or binary minus) need |
|
53 to be spaced properly; |
|
54 |
|
55 - existing occurrences of "1" may need to be constraint "1::nat" or |
|
56 even replaced by Suc 0; similar for old "2"; |
|
57 |
|
58 - replace "#nnn" by "nnn", and "#-nnn" by "-nnn"; |
|
59 |
|
60 - remove all special provisions on numerals in proofs; |
35 |
61 |
36 * HOL: linorder_less_split superseded by linorder_cases; |
62 * HOL: linorder_less_split superseded by linorder_cases; |
37 |
63 |
38 * HOL: added "The" definite description operator; move Hilbert's "Eps" |
64 * HOL: added "The" definite description operator; move Hilbert's "Eps" |
39 to peripheral theory "Hilbert_Choice"; |
65 to peripheral theory "Hilbert_Choice"; |