src/HOL/ex/Records.thy

   apply (tactic {*simp_tac 
            (HOL_basic_ss addsimprocs [Record.record_ex_sel_eq_simproc]) 1*})
   done
 
 
+subsection {* Some code generation *}
+
+export_code foo1 foo3 foo5 foo10 foo11 in SML file -
+
 end