changeset 30663 | 0b6aff7451b2 |
parent 29668 | 33ba3faeaa0e |
child 31077 | 28dd6fd3d184 |
--- a/src/HOL/Library/Nat_Infinity.thy Mon Mar 23 08:14:23 2009 +0100 +++ b/src/HOL/Library/Nat_Infinity.thy Mon Mar 23 08:14:24 2009 +0100 @@ -5,7 +5,7 @@ header {* Natural numbers with infinity *} theory Nat_Infinity -imports Plain "~~/src/HOL/Presburger" +imports Main begin subsection {* Type definition *}