--- a/src/HOL/Meson.thy Thu Nov 21 21:33:34 2013 +0100 +++ b/src/HOL/Meson.thy Thu Nov 21 21:33:34 2013 +0100 @@ -8,7 +8,7 @@ header {* MESON Proof Method *} theory Meson -imports Datatype +imports Nat begin subsection {* Negation Normal Form *}