src/HOL/Datatype.thy
changeset 21243 afffe1f72143
parent 21126 4dbc3ccbaab0
child 21404 eb85850d3eb7
--- a/src/HOL/Datatype.thy	Wed Nov 08 11:23:09 2006 +0100
+++ b/src/HOL/Datatype.thy	Wed Nov 08 13:48:29 2006 +0100
@@ -9,7 +9,7 @@
 header{*Analogues of the Cartesian Product and Disjoint Sum for Datatypes*}
 
 theory Datatype
-imports NatArith Sum_Type
+imports Nat Sum_Type
 begin
 
 typedef (Node)