src/HOL/Num.thy
changeset 55534 b18bdcbda41b
parent 55415 05f5fdb8d093
child 55974 c835a9379026
     1.1 --- a/src/HOL/Num.thy	Mon Feb 17 13:31:42 2014 +0100
     1.2 +++ b/src/HOL/Num.thy	Mon Feb 17 13:31:42 2014 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Binary Numerals *}
     1.5  
     1.6  theory Num
     1.7 -imports Datatype
     1.8 +imports Datatype BNF_LFP
     1.9  begin
    1.10  
    1.11  subsection {* The @{text num} type *}
    1.12 @@ -1249,4 +1249,3 @@
    1.13    code_module Num \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
    1.14  
    1.15  end
    1.16 -