src/HOL/ex/Records.thy
changeset 62119 b8c973d90ae7
parent 61933 cf58b5b794b2
child 67443 3abf6a722518
equal deleted inserted replaced
62118:e60f1a925b4d 62119:b8c973d90ae7
   321   bar3 :: 'c
   321   bar3 :: 'c
   322   bar21 :: "'b \<times> 'a"
   322   bar21 :: "'b \<times> 'a"
   323   bar32 :: "'c \<times> 'b"
   323   bar32 :: "'c \<times> 'b"
   324   bar31 :: "'c \<times> 'a"
   324   bar31 :: "'c \<times> 'a"
   325 
   325 
       
   326 print_record "('a,'b,'c) bar"
   326 
   327 
   327 subsection \<open>Some code generation\<close>
   328 subsection \<open>Some code generation\<close>
   328 
   329 
   329 export_code foo1 foo3 foo5 foo10 checking SML
   330 export_code foo1 foo3 foo5 foo10 checking SML
   330 
   331