added div/mod examples
authorhaftmann
Thu, 13 Dec 2007 07:09:04 +0100
changeset 25616 28d373f1482a
parent 25615 b337edd55a07
child 25617 b495384e48e1
added div/mod examples
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