src/HOL/Tools/numeral_syntax.ML
changeset 10891 890b117f6189
parent 10693 9e4a0e84d0d6
child 11488 4ff900551340
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Fri Jan 12 20:03:04 2001 +0100
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Fri Jan 12 20:03:26 2001 +0100
     1.3 @@ -9,8 +9,7 @@
     1.4  
     1.5  signature NUMERAL_SYNTAX =
     1.6  sig
     1.7 -  val dest_bin : term -> int
     1.8 -  val setup    : (theory -> theory) list
     1.9 +  val setup: (theory -> theory) list
    1.10  end;
    1.11  
    1.12  structure NumeralSyntax: NUMERAL_SYNTAX =