# HG changeset patch # User wenzelm # Date 1003968782 -7200 # Node ID 1accec985349ee46ce90b053045519cba1f830ba # Parent a77ad6c86564df70c8ef1b0c5778ef93088ab4ad * HOL/record: - provides cases/induct rules for use with corresponding Isar methods; - "record" operation truncates to particular fixed record (acts like a type cast); - make_defs no longer part of default simps; - internal definitions directly based on a light-weight abstract theory of product types over typedef rather than datatype; diff -r a77ad6c86564 -r 1accec985349 NEWS --- a/NEWS Thu Oct 25 02:12:10 2001 +0200 +++ b/NEWS Thu Oct 25 02:13:02 2001 +0200 @@ -97,6 +97,14 @@ - remove all special provisions on numerals in proofs; +* HOL/record: + - provides cases/induct rules for use with corresponding Isar methods; + - "record" operation truncates to particular fixed record (acts like + a type cast); + - make_defs no longer part of default simps; + - internal definitions directly based on a light-weight abstract + theory of product types over typedef rather than datatype; + * HOL: concrete setsum syntax "\i:A. b" == "setsum (%i. b) A" (beware of argument permutation!);