diff -r f6e595e4f608 -r 261cd8722677 src/HOL/Enum.thy --- a/src/HOL/Enum.thy Mon Sep 23 12:59:10 2024 +0200 +++ b/src/HOL/Enum.thy Mon Sep 23 13:32:38 2024 +0200 @@ -497,7 +497,7 @@ datatype (plugins only: code "quickcheck" extraction) finite_1 = a\<^sub>1 -notation (output) a\<^sub>1 ("a\<^sub>1") +notation (output) a\<^sub>1 (\a\<^sub>1\) lemma UNIV_finite_1: "UNIV = {a\<^sub>1}" @@ -601,8 +601,8 @@ datatype (plugins only: code "quickcheck" extraction) finite_2 = a\<^sub>1 | a\<^sub>2 -notation (output) a\<^sub>1 ("a\<^sub>1") -notation (output) a\<^sub>2 ("a\<^sub>2") +notation (output) a\<^sub>1 (\a\<^sub>1\) +notation (output) a\<^sub>2 (\a\<^sub>2\) lemma UNIV_finite_2: "UNIV = {a\<^sub>1, a\<^sub>2}" @@ -730,9 +730,9 @@ datatype (plugins only: code "quickcheck" extraction) finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 -notation (output) a\<^sub>1 ("a\<^sub>1") -notation (output) a\<^sub>2 ("a\<^sub>2") -notation (output) a\<^sub>3 ("a\<^sub>3") +notation (output) a\<^sub>1 (\a\<^sub>1\) +notation (output) a\<^sub>2 (\a\<^sub>2\) +notation (output) a\<^sub>3 (\a\<^sub>3\) lemma UNIV_finite_3: "UNIV = {a\<^sub>1, a\<^sub>2, a\<^sub>3}" @@ -971,10 +971,10 @@ datatype (plugins only: code "quickcheck" extraction) finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 -notation (output) a\<^sub>1 ("a\<^sub>1") -notation (output) a\<^sub>2 ("a\<^sub>2") -notation (output) a\<^sub>3 ("a\<^sub>3") -notation (output) a\<^sub>4 ("a\<^sub>4") +notation (output) a\<^sub>1 (\a\<^sub>1\) +notation (output) a\<^sub>2 (\a\<^sub>2\) +notation (output) a\<^sub>3 (\a\<^sub>3\) +notation (output) a\<^sub>4 (\a\<^sub>4\) lemma UNIV_finite_4: "UNIV = {a\<^sub>1, a\<^sub>2, a\<^sub>3, a\<^sub>4}" @@ -1060,11 +1060,11 @@ datatype (plugins only: code "quickcheck" extraction) finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5 -notation (output) a\<^sub>1 ("a\<^sub>1") -notation (output) a\<^sub>2 ("a\<^sub>2") -notation (output) a\<^sub>3 ("a\<^sub>3") -notation (output) a\<^sub>4 ("a\<^sub>4") -notation (output) a\<^sub>5 ("a\<^sub>5") +notation (output) a\<^sub>1 (\a\<^sub>1\) +notation (output) a\<^sub>2 (\a\<^sub>2\) +notation (output) a\<^sub>3 (\a\<^sub>3\) +notation (output) a\<^sub>4 (\a\<^sub>4\) +notation (output) a\<^sub>5 (\a\<^sub>5\) lemma UNIV_finite_5: "UNIV = {a\<^sub>1, a\<^sub>2, a\<^sub>3, a\<^sub>4, a\<^sub>5}"