changeset 15131 | c69542757a4d |
parent 15013 | 34264f5e4691 |
child 15140 | 322485b816ac |
--- a/src/HOL/Integ/Numeral.thy Mon Aug 16 14:21:54 2004 +0200 +++ b/src/HOL/Integ/Numeral.thy Mon Aug 16 14:22:27 2004 +0200 @@ -6,8 +6,10 @@ header{*Arithmetic on Binary Integers*} -theory Numeral = IntDef -files "Tools/numeral_syntax.ML": +theory Numeral +import IntDef +files "Tools/numeral_syntax.ML" +begin text{* The file @{text numeral_syntax.ML} hides the constructors Pls and Min. Only qualified access Numeral.Pls and Numeral.Min is allowed.