# HG changeset patch
# User bulwahn
# Date 1291362046 -3600
# Node ID 1d5f76d798564a701cb75a8a0bc1c0606cb30d9a
# Parent  ef6fde932f4cab2f5bf363ca71ea46383b989411
adding shorter output syntax for the finite types of quickcheck

diff -r ef6fde932f4c -r 1d5f76d79856 src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Fri Dec 03 08:40:46 2010 +0100
+++ b/src/HOL/Enum.thy	Fri Dec 03 08:40:46 2010 +0100
@@ -318,6 +318,8 @@
 
 datatype finite_1 = a\<^isub>1
 
+notation (output) a\<^isub>1  ("a\<^isub>1")
+
 instantiation finite_1 :: enum
 begin
 
@@ -352,6 +354,9 @@
 
 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")
+
 instantiation finite_2 :: enum
 begin
 
@@ -388,6 +393,10 @@
 
 datatype finite_3 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3
 
+notation (output) a\<^isub>1  ("a\<^isub>1")
+notation (output) a\<^isub>2  ("a\<^isub>2")
+notation (output) a\<^isub>3  ("a\<^isub>3")
+
 instantiation finite_3 :: enum
 begin
 
@@ -422,6 +431,11 @@
 
 datatype finite_4 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4
 
+notation (output) a\<^isub>1  ("a\<^isub>1")
+notation (output) a\<^isub>2  ("a\<^isub>2")
+notation (output) a\<^isub>3  ("a\<^isub>3")
+notation (output) a\<^isub>4  ("a\<^isub>4")
+
 instantiation finite_4 :: enum
 begin
 
@@ -438,6 +452,12 @@
 
 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")
+notation (output) a\<^isub>2  ("a\<^isub>2")
+notation (output) a\<^isub>3  ("a\<^isub>3")
+notation (output) a\<^isub>4  ("a\<^isub>4")
+notation (output) a\<^isub>5  ("a\<^isub>5")
+
 instantiation finite_5 :: enum
 begin