adding shorter output syntax for the finite types of quickcheck
authorbulwahn
Fri Dec 03 08:40:46 2010 +0100 (2010-12-03)
changeset 409001d5f76d79856
parent 40899 ef6fde932f4c
child 40901 8fdfa9c4e7ed
adding shorter output syntax for the finite types of quickcheck
src/HOL/Enum.thy
     1.1 --- a/src/HOL/Enum.thy	Fri Dec 03 08:40:46 2010 +0100
     1.2 +++ b/src/HOL/Enum.thy	Fri Dec 03 08:40:46 2010 +0100
     1.3 @@ -318,6 +318,8 @@
     1.4  
     1.5  datatype finite_1 = a\<^isub>1
     1.6  
     1.7 +notation (output) a\<^isub>1  ("a\<^isub>1")
     1.8 +
     1.9  instantiation finite_1 :: enum
    1.10  begin
    1.11  
    1.12 @@ -352,6 +354,9 @@
    1.13  
    1.14  datatype finite_2 = a\<^isub>1 | a\<^isub>2
    1.15  
    1.16 +notation (output) a\<^isub>1  ("a\<^isub>1")
    1.17 +notation (output) a\<^isub>2  ("a\<^isub>2")
    1.18 +
    1.19  instantiation finite_2 :: enum
    1.20  begin
    1.21  
    1.22 @@ -388,6 +393,10 @@
    1.23  
    1.24  datatype finite_3 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3
    1.25  
    1.26 +notation (output) a\<^isub>1  ("a\<^isub>1")
    1.27 +notation (output) a\<^isub>2  ("a\<^isub>2")
    1.28 +notation (output) a\<^isub>3  ("a\<^isub>3")
    1.29 +
    1.30  instantiation finite_3 :: enum
    1.31  begin
    1.32  
    1.33 @@ -422,6 +431,11 @@
    1.34  
    1.35  datatype finite_4 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4
    1.36  
    1.37 +notation (output) a\<^isub>1  ("a\<^isub>1")
    1.38 +notation (output) a\<^isub>2  ("a\<^isub>2")
    1.39 +notation (output) a\<^isub>3  ("a\<^isub>3")
    1.40 +notation (output) a\<^isub>4  ("a\<^isub>4")
    1.41 +
    1.42  instantiation finite_4 :: enum
    1.43  begin
    1.44  
    1.45 @@ -438,6 +452,12 @@
    1.46  
    1.47  datatype finite_5 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4 | a\<^isub>5
    1.48  
    1.49 +notation (output) a\<^isub>1  ("a\<^isub>1")
    1.50 +notation (output) a\<^isub>2  ("a\<^isub>2")
    1.51 +notation (output) a\<^isub>3  ("a\<^isub>3")
    1.52 +notation (output) a\<^isub>4  ("a\<^isub>4")
    1.53 +notation (output) a\<^isub>5  ("a\<^isub>5")
    1.54 +
    1.55  instantiation finite_5 :: enum
    1.56  begin
    1.57