399 datatypes and sets, as well as recursive functions; can be invoked |
399 datatypes and sets, as well as recursive functions; can be invoked |
400 via 'generate_code' theory section; |
400 via 'generate_code' theory section; |
401 |
401 |
402 * HOL: canonical cases/induct rules for n-tuples (n = 3..7); |
402 * HOL: canonical cases/induct rules for n-tuples (n = 3..7); |
403 |
403 |
|
404 * HOL: consolidated and renamed several theories. In particular: |
|
405 Ord.thy has been absorbed into HOL.thy |
|
406 String.thy has been absorbed into List.thy |
|
407 |
404 * HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A" |
408 * HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A" |
405 (beware of argument permutation!); |
409 (beware of argument permutation!); |
406 |
410 |
407 * HOL: linorder_less_split superseded by linorder_cases; |
411 * HOL: linorder_less_split superseded by linorder_cases; |
408 |
412 |
409 * HOL/List: "nodups" renamed to "distinct"; |
413 * HOL/List: "nodups" renamed to "distinct"; |
410 |
414 |
411 * HOL: added "The" definite description operator; move Hilbert's "Eps" |
415 * HOL: added "The" definite description operator; move Hilbert's "Eps" |
412 to peripheral theory "Hilbert_Choice"; |
416 to peripheral theory "Hilbert_Choice"; some INCOMPATIBILITIES: |
|
417 - Ex_def has changed, now need to use some_eq_ex |
413 |
418 |
414 * HOL: made split_all_tac safe; EXISTING PROOFS MAY FAIL OR LOOP, so |
419 * HOL: made split_all_tac safe; EXISTING PROOFS MAY FAIL OR LOOP, so |
415 in this (rare) case use: |
420 in this (rare) case use: |
416 |
421 |
417 delSWrapper "split_all_tac" |
422 delSWrapper "split_all_tac" |