src/HOL/Enum.thy

 apply (metis finite_1.exhaust)
 done
 
 end
 
+hide_const a\<^isub>1
+
 datatype finite_2 = a\<^isub>1 | a\<^isub>2
 
 instantiation finite_2 :: enum
 begin
 

 apply (metis finite_2.distinct finite_2.nchotomy)+
 done
 
 end
 
+hide_const a\<^isub>1 a\<^isub>2
+
 
 datatype finite_3 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3
 
 instantiation finite_3 :: enum
 begin

 instance proof (intro_classes)
 qed (auto simp add: less_finite_3_def less_eq_finite_3_def split: finite_3.split_asm)
 
 end
 
+hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3
+
 
 datatype finite_4 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4
 
 instantiation finite_4 :: enum
 begin

 instance proof
 qed (auto simp add: enum_finite_4_def intro: finite_4.exhaust)
 
 end
 
+hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4
 
 
 datatype finite_5 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4 | a\<^isub>5
 
 instantiation finite_5 :: enum

 
 instance proof
 qed (auto simp add: enum_finite_5_def intro: finite_5.exhaust)
 
 end
+
+hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
+
 
 hide_type finite_1 finite_2 finite_3 finite_4 finite_5
 hide_const (open) n_lists product
 
 end