small adjustments
authorhaftmann
Sun Jul 23 07:21:41 2006 +0200 (2006-07-23)
changeset 20187af47971ea304
parent 20186 56207a6f4cc5
child 20188 8b22026445af
small adjustments
src/HOL/ex/Classpackage.thy
src/HOL/ex/Codegenerator.thy
     1.1 --- a/src/HOL/ex/Classpackage.thy	Sun Jul 23 07:21:22 2006 +0200
     1.2 +++ b/src/HOL/ex/Classpackage.thy	Sun Jul 23 07:21:41 2006 +0200
     1.3 @@ -312,7 +312,6 @@
     1.4  code_generate (ml, haskell) x
     1.5  code_generate (ml, haskell) y
     1.6  
     1.7 -code_serialize ml (_)
     1.8  code_serialize ml (-)
     1.9  
    1.10  end
     2.1 --- a/src/HOL/ex/Codegenerator.thy	Sun Jul 23 07:21:22 2006 +0200
     2.2 +++ b/src/HOL/ex/Codegenerator.thy	Sun Jul 23 07:21:41 2006 +0200
     2.3 @@ -2,7 +2,7 @@
     2.4      Author:     Florian Haftmann, TU Muenchen
     2.5  *)
     2.6  
     2.7 -header {* Test and Examples for Code Generator *}
     2.8 +header {* Test and Examples for code generator *}
     2.9  
    2.10  theory Codegenerator
    2.11  imports Main
    2.12 @@ -46,6 +46,8 @@
    2.13  
    2.14  code_generate (ml, haskell) Pair fst snd Let split swap swapp appl
    2.15  
    2.16 +subsection {* integers *}
    2.17 +
    2.18  definition
    2.19    k :: "int"
    2.20    "k = 42"
    2.21 @@ -64,6 +66,8 @@
    2.22    "op < :: int \<Rightarrow> int \<Rightarrow> bool"
    2.23    "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
    2.24    fac
    2.25 +  "op div :: int \<Rightarrow> int \<Rightarrow> int"
    2.26 +  "op mod :: int \<Rightarrow> int \<Rightarrow> int"  
    2.27  
    2.28  subsection {* sums *}
    2.29