changeset 80864 | 1b1f77bcee5f |
parent 80703 | cc4ecaa8e96e |
--- a/src/HOL/Examples/Records.thy Wed Sep 11 22:28:42 2024 +0200 +++ b/src/HOL/Examples/Records.thy Wed Sep 11 22:56:42 2024 +0200 @@ -374,7 +374,7 @@ bar32 :: "'c \<times> 'b" bar31 :: "'c \<times> 'a" -print_record "('a,'b,'c) bar" +print_record "('a, 'b, 'c) bar" subsection \<open>Some code generation\<close>