Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
* HOL/record:
authorwenzelm
Thu, 25 Oct 2001 02:13:02 +0200
changeset 11930 1accec985349
parent 11929 a77ad6c86564
child 11931 a5d1c9b34900
* 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;
NEWS file | annotate | diff | comparison | revisions 
--- 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 "\<Sum>i:A. b" == "setsum (%i. b) A"
 (beware of argument permutation!);
isabelle