--- a/src/HOL/Enum.thy Mon Nov 22 11:35:06 2010 +0100
+++ b/src/HOL/Enum.thy Mon Nov 22 11:35:07 2010 +0100
@@ -348,6 +348,8 @@
end
+hide_const a\<^isub>1
+
datatype finite_2 = a\<^isub>1 | a\<^isub>2
instantiation finite_2 :: enum
@@ -381,6 +383,8 @@
end
+hide_const a\<^isub>1 a\<^isub>2
+
datatype finite_3 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3
@@ -413,6 +417,8 @@
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
@@ -427,6 +433,7 @@
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
@@ -442,6 +449,9 @@
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