src/ZF/ex/Enum.ML

     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
 Example of a BIG enumeration type
 
-Can go up to at least 100 constructors, but it takes over 10 minutes...
+Can go up to at least 100 constructors, but it takes nearly 7 minutes...
 *)
 
 
-(*An enumeration type with 60 contructors!  -- takes about 214 seconds!*)
+(*An enumeration type with 60 contructors!  -- takes about 150 seconds!*)
 fun mk_ids a 0 = []
   | mk_ids a n = a :: mk_ids (bump_string a) (n-1);
 
 val consts = mk_ids "con1" 60;
 

   val monos = [];
   val type_intrs = data_typechecks
   val type_elims = []);
 
 goal Enum.thy "con59 ~= con60";
-by (simp_tac (ZF_ss addsimps Enum.free_iffs) 1);  (*2.3 secs*)
+by (simp_tac (ZF_ss addsimps Enum.free_iffs) 1);
 result();