hiding the constants
authorbulwahn
Mon Nov 22 11:35:07 2010 +0100 (2010-11-22)
changeset 4065758a6ba7ccfc5
parent 40656 36ca3fad1f31
child 40658 5ccfc3ee7fe6
hiding the constants
src/HOL/Enum.thy
     1.1 --- a/src/HOL/Enum.thy	Mon Nov 22 11:35:06 2010 +0100
     1.2 +++ b/src/HOL/Enum.thy	Mon Nov 22 11:35:07 2010 +0100
     1.3 @@ -348,6 +348,8 @@
     1.4  
     1.5  end
     1.6  
     1.7 +hide_const a\<^isub>1
     1.8 +
     1.9  datatype finite_2 = a\<^isub>1 | a\<^isub>2
    1.10  
    1.11  instantiation finite_2 :: enum
    1.12 @@ -381,6 +383,8 @@
    1.13  
    1.14  end
    1.15  
    1.16 +hide_const a\<^isub>1 a\<^isub>2
    1.17 +
    1.18  
    1.19  datatype finite_3 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3
    1.20  
    1.21 @@ -413,6 +417,8 @@
    1.22  
    1.23  end
    1.24  
    1.25 +hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3
    1.26 +
    1.27  
    1.28  datatype finite_4 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4
    1.29  
    1.30 @@ -427,6 +433,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  
    1.36  
    1.37  datatype finite_5 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4 | a\<^isub>5
    1.38 @@ -442,6 +449,9 @@
    1.39  
    1.40  end
    1.41  
    1.42 +hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
    1.43 +
    1.44 +
    1.45  hide_type finite_1 finite_2 finite_3 finite_4 finite_5
    1.46  hide_const (open) n_lists product
    1.47