# HG changeset patch
# User haftmann
# Date 1197526144 -3600
# Node ID 28d373f1482a6771a6790a278e4a6a5d4d35a427
# Parent  b337edd55a079b7413a44799fa650f47ecc49fc4
added div/mod examples

diff -r b337edd55a07 -r 28d373f1482a src/HOL/ex/Codegenerator_Pretty.thy
--- a/src/HOL/ex/Codegenerator_Pretty.thy	Thu Dec 13 07:09:03 2007 +0100
+++ b/src/HOL/ex/Codegenerator_Pretty.thy	Thu Dec 13 07:09:04 2007 +0100
@@ -49,9 +49,12 @@
 definition
   "foobar' = (foo' R1' 1 R3', bar' R2' 0 R3', foo' R1' R3' R2')"
 
-export_code foobar foobar' in SML module_name Foo
+definition
+  "(doodle :: nat) = 1705 div 42 * 42 + 1705 mod 42"
+
+export_code foobar foobar' doodle in SML module_name Foo
   in OCaml file -
   in Haskell file -
-ML {* (Foo.foobar, Foo.foobar') *}
+ML {* (Foo.foobar, Foo.foobar', Foo.doodle) *}
 
 end