src/HOL/Enum.thy

 apply (metis finite_1.exhaust)
 done
 
 end
 
-hide_const a\<^isub>1
+hide_const (open) a\<^isub>1
 
 datatype finite_2 = a\<^isub>1 | a\<^isub>2
 
 notation (output) a\<^isub>1  ("a\<^isub>1")
 notation (output) a\<^isub>2  ("a\<^isub>2")

 apply (metis finite_2.distinct finite_2.nchotomy)+
 done
 
 end
 
-hide_const a\<^isub>1 a\<^isub>2
+hide_const (open) a\<^isub>1 a\<^isub>2
 
 
 datatype finite_3 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3
 
 notation (output) a\<^isub>1  ("a\<^isub>1")

 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
+hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3
 
 
 datatype finite_4 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4
 
 notation (output) a\<^isub>1  ("a\<^isub>1")

     by (auto, case_tac x) auto
 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
+hide_const (open) 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
 
 notation (output) a\<^isub>1  ("a\<^isub>1")

     by (auto, case_tac x) auto
 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) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
+
+
+hide_type (open) finite_1 finite_2 finite_3 finite_4 finite_5
 hide_const (open) enum enum_all enum_ex n_lists all_n_lists ex_n_lists product
 
 end