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.
merged
authorwenzelm
Mon, 09 Dec 2013 23:16:10 +0100
changeset 54710 afdb394ee0c0
parent 54708 8e71c6ed4d74 (diff)
parent 54709 87402674fe2f (current diff)
child 54711 15a642b9ffac
merged
--- a/NEWS	Mon Dec 09 22:02:42 2013 +0100
+++ b/NEWS	Mon Dec 09 23:16:10 2013 +0100
@@ -24,6 +24,9 @@
 
 *** HOL ***
 
+* Code generations are provided for make, fields, extend and truncate
+operations on records.
+
 * Qualified constant names Wellfounded.acc, Wellfounded.accp.
 INCOMPATIBILITY.
 
--- a/src/HOL/Tools/record.ML	Mon Dec 09 22:02:42 2013 +0100
+++ b/src/HOL/Tools/record.ML	Mon Dec 09 23:16:10 2013 +0100
@@ -2007,7 +2007,8 @@
           ||>> (Global_Theory.add_defs false o
                 map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) upd_specs
           ||>> (Global_Theory.add_defs false o
-                map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
+                map (rpair [Code.add_default_eqn_attribute]
+                o apfst (Binding.conceal o Binding.name))) (*FIXME Spec_Rules (?)*)
             [make_spec, fields_spec, extend_spec, truncate_spec]);
 
     (* prepare propositions *)
isabelle