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.
hide base name of "make", "fields", "extend", "truncate", "more",
authorwenzelm
Fri, 21 Dec 2001 23:18:27 +0100
changeset 12590 3573830e9b91
parent 12589 afc6ffffeb11
child 12591 5a46569d2b05
hide base name of "make", "fields", "extend", "truncate", "more", "more_update";
src/HOL/Tools/record_package.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/record_package.ML	Fri Dec 21 23:17:35 2001 +0100
+++ b/src/HOL/Tools/record_package.ML	Fri Dec 21 23:18:27 2001 +0100
@@ -848,7 +848,9 @@
       |> (PureThy.add_defs_i false o map Thm.no_attributes) sel_specs
       |>>> (PureThy.add_defs_i false o map Thm.no_attributes) update_specs
       |>>> (PureThy.add_defs_i false o map Thm.no_attributes)
-        [make_spec, fields_spec, extend_spec, truncate_spec];
+        [make_spec, fields_spec, extend_spec, truncate_spec]
+      |>> Theory.hide_consts false [full makeN, full fieldsN, full extendN, full truncateN,
+        full moreN, full (suffix updateN moreN)];
 
 
     (* 3rd stage: thms_thy *)
isabelle