src/HOL/ex/Records.thy
changeset 62119 b8c973d90ae7
parent 61933 cf58b5b794b2
child 67443 3abf6a722518
--- a/src/HOL/ex/Records.thy	Sun Jan 10 19:46:31 2016 -0800
+++ b/src/HOL/ex/Records.thy	Sun Jan 10 20:13:29 2016 -0800
@@ -323,6 +323,7 @@
   bar32 :: "'c \<times> 'b"
   bar31 :: "'c \<times> 'a"
 
+print_record "('a,'b,'c) bar"
 
 subsection \<open>Some code generation\<close>