src/HOL/Enum.thy
changeset 41085 a549ff1d4070
parent 41078 051251fde456
child 41115 2c362ff5daf4
     1.1 --- a/src/HOL/Enum.thy	Wed Dec 08 16:47:57 2010 +0100
     1.2 +++ b/src/HOL/Enum.thy	Wed Dec 08 18:07:03 2010 +0100
     1.3 @@ -545,7 +545,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -hide_const a\<^isub>1
     1.8 +hide_const (open) a\<^isub>1
     1.9  
    1.10  datatype finite_2 = a\<^isub>1 | a\<^isub>2
    1.11  
    1.12 @@ -598,7 +598,7 @@
    1.13  
    1.14  end
    1.15  
    1.16 -hide_const a\<^isub>1 a\<^isub>2
    1.17 +hide_const (open) a\<^isub>1 a\<^isub>2
    1.18  
    1.19  
    1.20  datatype finite_3 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3
    1.21 @@ -651,7 +651,7 @@
    1.22  
    1.23  end
    1.24  
    1.25 -hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3
    1.26 +hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3
    1.27  
    1.28  
    1.29  datatype finite_4 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4
    1.30 @@ -687,7 +687,7 @@
    1.31  
    1.32  end
    1.33  
    1.34 -hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4
    1.35 +hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4
    1.36  
    1.37  
    1.38  datatype finite_5 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4 | a\<^isub>5
    1.39 @@ -724,10 +724,10 @@
    1.40  
    1.41  end
    1.42  
    1.43 -hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
    1.44 +hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
    1.45  
    1.46  
    1.47 -hide_type finite_1 finite_2 finite_3 finite_4 finite_5
    1.48 +hide_type (open) finite_1 finite_2 finite_3 finite_4 finite_5
    1.49  hide_const (open) enum enum_all enum_ex n_lists all_n_lists ex_n_lists product
    1.50  
    1.51  end