src/ZF/Finite.thy
changeset 12175 5cf58a1799a7
parent 9491 1a36151ee2fc
child 12214 f368821d9c68
     1.1 --- a/src/ZF/Finite.thy	Tue Nov 13 22:20:15 2001 +0100
     1.2 +++ b/src/ZF/Finite.thy	Tue Nov 13 22:20:51 2001 +0100
     1.3 @@ -8,8 +8,6 @@
     1.4  
     1.5  Finite = Inductive + Nat +
     1.6  
     1.7 -setup setup_datatypes
     1.8 -
     1.9  (*The natural numbers as a datatype*)
    1.10  rep_datatype 
    1.11    elim		natE