# HG changeset patch
# User haftmann
# Date 1257948629 -3600
# Node ID ad27f52ee759c2770678be413bfc57f910d2aa0a
# Parent  2640cc1cfc2ed076cb6f8d165fe2d1cca432026f
explicit invocation of code generation

diff -r 2640cc1cfc2e -r ad27f52ee759 src/HOL/ex/Records.thy
--- a/src/HOL/ex/Records.thy	Wed Nov 11 15:10:26 2009 +0100
+++ b/src/HOL/ex/Records.thy	Wed Nov 11 15:10:29 2009 +0100
@@ -334,4 +334,8 @@
   done
 
 
+subsection {* Some code generation *}
+
+export_code foo1 foo3 foo5 foo10 foo11 in SML file -
+
 end