src/HOL/Numeral.thy
changeset 23708 b5eb0b4dd17d
parent 23574 42765aff66d6
child 23855 b1a754e544b6
     1.1 --- a/src/HOL/Numeral.thy	Tue Jul 10 17:30:47 2007 +0200
     1.2 +++ b/src/HOL/Numeral.thy	Tue Jul 10 17:30:49 2007 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  header {* Arithmetic on Binary Integers *}
     1.5  
     1.6  theory Numeral
     1.7 -imports IntDef
     1.8 +imports Datatype IntDef
     1.9  uses
    1.10    ("Tools/numeral.ML")
    1.11    ("Tools/numeral_syntax.ML")