changeset 23146 | 0bc590051d95 |
parent 21781 | 8314ebb5364d |
child 24630 | 351a308ab58d |
--- a/src/ZF/Tools/numeral_syntax.ML Thu May 31 11:00:06 2007 +0200 +++ b/src/ZF/Tools/numeral_syntax.ML Thu May 31 12:06:31 2007 +0200 @@ -3,7 +3,7 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Concrete syntax for generic numerals. Assumes consts and syntax of -theory ZF/Integ/Bin. +theory Bin. *) signature NUMERAL_SYNTAX =