src/HOL/ex/Records.thy
changeset 34971 5c290f56ebf7
parent 33613 ad27f52ee759
child 37826 4c0a5e35931a
equal deleted inserted replaced
34970:4c316d777461 34971:5c290f56ebf7
   332   apply (tactic {*simp_tac 
   332   apply (tactic {*simp_tac 
   333            (HOL_basic_ss addsimprocs [Record.record_ex_sel_eq_simproc]) 1*})
   333            (HOL_basic_ss addsimprocs [Record.record_ex_sel_eq_simproc]) 1*})
   334   done
   334   done
   335 
   335 
   336 
   336 
       
   337 subsection {* A more complex record expression *}
       
   338 
       
   339 record ('a, 'b, 'c) bar = bar1 :: 'a
       
   340   bar2 :: 'b
       
   341   bar3 :: 'c
       
   342   bar21 :: "'b \<times> 'a"
       
   343   bar32 :: "'c \<times> 'b"
       
   344   bar31 :: "'c \<times> 'a"
       
   345 
       
   346 
   337 subsection {* Some code generation *}
   347 subsection {* Some code generation *}
   338 
   348 
   339 export_code foo1 foo3 foo5 foo10 foo11 in SML file -
   349 export_code foo1 foo3 foo5 foo10 foo11 in SML file -
   340 
   350 
   341 end
   351 end