slight adaptions
authorhaftmann
Wed Jun 14 12:13:12 2006 +0200 (2006-06-14)
changeset 198882b4c09941e04
parent 19887 e3a03f1f54eb
child 19889 2202a5648897
slight adaptions
src/HOL/ex/Classpackage.thy
src/HOL/ex/Codegenerator.thy
     1.1 --- a/src/HOL/ex/Classpackage.thy	Wed Jun 14 12:12:37 2006 +0200
     1.2 +++ b/src/HOL/ex/Classpackage.thy	Wed Jun 14 12:13:12 2006 +0200
     1.3 @@ -314,9 +314,9 @@
     1.4    "x = ((2::nat) \<otimes> \<one> \<otimes> 3, (2::int) \<otimes> \<one> \<otimes> \<div> 3, [1::nat, 2] \<otimes> \<one> \<otimes> [1, 2, 3])"
     1.5    "y = (2 :: int, \<div> 2 :: int) \<otimes> \<one> \<otimes> (3, \<div> 3)"
     1.6  
     1.7 -code_generate "op \<otimes>" "\<one>" "inv"
     1.8 -code_generate x
     1.9 -code_generate y
    1.10 +code_generate (ml, haskell) "op \<otimes>" "\<one>" "inv"
    1.11 +code_generate (ml, haskell) x
    1.12 +code_generate (ml, haskell) y
    1.13  
    1.14  code_serialize ml (-)
    1.15  
     2.1 --- a/src/HOL/ex/Codegenerator.thy	Wed Jun 14 12:12:37 2006 +0200
     2.2 +++ b/src/HOL/ex/Codegenerator.thy	Wed Jun 14 12:13:12 2006 +0200
     2.3 @@ -14,7 +14,7 @@
     2.4    xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
     2.5    "xor p q = ((p | q) & \<not> (p & q))"
     2.6  
     2.7 -code_generate (ml) xor
     2.8 +code_generate (ml, haskell) xor
     2.9  
    2.10  subsection {* natural numbers *}
    2.11  
    2.12 @@ -24,9 +24,9 @@
    2.13    n :: nat
    2.14    "n = 42"
    2.15  
    2.16 -code_generate (ml) n
    2.17 +code_generate (ml, haskell) n
    2.18  
    2.19 -code_generate (ml)
    2.20 +code_generate (ml, haskell)
    2.21    "0::nat" "one" n
    2.22    "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
    2.23    "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
    2.24 @@ -44,7 +44,7 @@
    2.25    appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b"
    2.26    "appl p = (let (f, x) = p in f x)"
    2.27  
    2.28 -code_generate (ml) Pair fst snd Let split swap swapp appl
    2.29 +code_generate (ml, haskell) Pair fst snd Let split swap swapp appl
    2.30  
    2.31  definition
    2.32    k :: "int"
    2.33 @@ -56,7 +56,7 @@
    2.34  recdef fac "measure nat"
    2.35    "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))"
    2.36  
    2.37 -code_generate (ml)
    2.38 +code_generate (ml, haskell)
    2.39    "0::int" k
    2.40    "op + :: int \<Rightarrow> int \<Rightarrow> int"
    2.41    "op - :: int \<Rightarrow> int \<Rightarrow> int"
    2.42 @@ -67,11 +67,11 @@
    2.43  
    2.44  subsection {* sums *}
    2.45  
    2.46 -code_generate (ml) Inl Inr
    2.47 +code_generate (ml, haskell) Inl Inr
    2.48  
    2.49  subsection {* options *}
    2.50  
    2.51 -code_generate (ml) None Some
    2.52 +code_generate (ml, haskell) None Some
    2.53  
    2.54  subsection {* lists *}
    2.55  
    2.56 @@ -81,7 +81,7 @@
    2.57    qs :: "nat list"
    2.58    "qs == rev ps"
    2.59  
    2.60 -code_generate (ml) hd tl "op @" ps qs
    2.61 +code_generate (ml, haskell) hd tl "op @" ps qs
    2.62  
    2.63  subsection {* mutual datatypes *}
    2.64  
    2.65 @@ -98,11 +98,11 @@
    2.66    "mut2 mut2.Tip = mut2.Tip"
    2.67    "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
    2.68  
    2.69 -code_generate (ml) mut1 mut2
    2.70 +code_generate (ml, haskell) mut1 mut2
    2.71  
    2.72  subsection {* equalities *}
    2.73  
    2.74 -code_generate (ml)
    2.75 +code_generate (ml, haskell)
    2.76    "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
    2.77    "op = :: nat \<Rightarrow> nat \<Rightarrow> bool"
    2.78    "op = :: int \<Rightarrow> int \<Rightarrow> bool"
    2.79 @@ -129,7 +129,7 @@
    2.80    "Codegenerator.g" "Mymod.A.f"
    2.81    "Codegenerator.h" "Mymod.A.B.f"
    2.82  
    2.83 -code_generate (ml) f g h
    2.84 +code_generate (ml, haskell) f g h
    2.85  
    2.86  code_serialize ml (-)
    2.87