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