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 consts in Numeral.thy;
authorwenzelm
Sun, 09 Apr 2006 18:51:15 +0200
changeset 19381 6cd8abc7f15b
parent 19380 b808efaa5828
child 19382 44937faf9e1a
hide consts in Numeral.thy;
src/HOL/Tools/numeral_syntax.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/numeral_syntax.ML	Sun Apr 09 18:51:13 2006 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML	Sun Apr 09 18:51:15 2006 +0200
@@ -55,8 +55,6 @@
 (* theory setup *)
 
 val setup =
-  Theory.hide_consts_i false ["Numeral.Pls", "Numeral.Min"] #>
-  Theory.hide_consts_i false ["Numeral.bit.B0", "Numeral.bit.B1"] #>
   Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
   Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')];
isabelle