explicit invocation of code generation
authorhaftmann
Wed Nov 11 15:10:29 2009 +0100 (2009-11-11)
changeset 33613ad27f52ee759
parent 33612 2640cc1cfc2e
child 33614 ecc90891c474
explicit invocation of code generation
src/HOL/ex/Records.thy
     1.1 --- a/src/HOL/ex/Records.thy	Wed Nov 11 15:10:26 2009 +0100
     1.2 +++ b/src/HOL/ex/Records.thy	Wed Nov 11 15:10:29 2009 +0100
     1.3 @@ -334,4 +334,8 @@
     1.4    done
     1.5  
     1.6  
     1.7 +subsection {* Some code generation *}
     1.8 +
     1.9 +export_code foo1 foo3 foo5 foo10 foo11 in SML file -
    1.10 +
    1.11  end