# HG changeset patch
# User haftmann
# Date 1153632101 -7200
# Node ID af47971ea30493a09765b275f45d6eacbcb30bd5
# Parent  56207a6f4cc5831e15c4381633c8793ff4a90e5f
small adjustments

diff -r 56207a6f4cc5 -r af47971ea304 src/HOL/ex/Classpackage.thy
--- a/src/HOL/ex/Classpackage.thy	Sun Jul 23 07:21:22 2006 +0200
+++ b/src/HOL/ex/Classpackage.thy	Sun Jul 23 07:21:41 2006 +0200
@@ -312,7 +312,6 @@
 code_generate (ml, haskell) x
 code_generate (ml, haskell) y
 
-code_serialize ml (_)
 code_serialize ml (-)
 
 end
diff -r 56207a6f4cc5 -r af47971ea304 src/HOL/ex/Codegenerator.thy
--- a/src/HOL/ex/Codegenerator.thy	Sun Jul 23 07:21:22 2006 +0200
+++ b/src/HOL/ex/Codegenerator.thy	Sun Jul 23 07:21:41 2006 +0200
@@ -2,7 +2,7 @@
     Author:     Florian Haftmann, TU Muenchen
 *)
 
-header {* Test and Examples for Code Generator *}
+header {* Test and Examples for code generator *}
 
 theory Codegenerator
 imports Main
@@ -46,6 +46,8 @@
 
 code_generate (ml, haskell) Pair fst snd Let split swap swapp appl
 
+subsection {* integers *}
+
 definition
   k :: "int"
   "k = 42"
@@ -64,6 +66,8 @@
   "op < :: int \<Rightarrow> int \<Rightarrow> bool"
   "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
   fac
+  "op div :: int \<Rightarrow> int \<Rightarrow> int"
+  "op mod :: int \<Rightarrow> int \<Rightarrow> int"  
 
 subsection {* sums *}