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 -