src/HOL/ex/Codegenerator.thy
 changeset 19888 2b4c09941e04 parent 19817 bb16bf9ae3fd child 20187 af47971ea304
```     1.1 --- a/src/HOL/ex/Codegenerator.thy	Wed Jun 14 12:12:37 2006 +0200
1.2 +++ b/src/HOL/ex/Codegenerator.thy	Wed Jun 14 12:13:12 2006 +0200
1.3 @@ -14,7 +14,7 @@
1.4    xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
1.5    "xor p q = ((p | q) & \<not> (p & q))"
1.6
1.7 -code_generate (ml) xor
1.9
1.10  subsection {* natural numbers *}
1.11
1.12 @@ -24,9 +24,9 @@
1.13    n :: nat
1.14    "n = 42"
1.15
1.16 -code_generate (ml) n
1.18
1.19 -code_generate (ml)
1.21    "0::nat" "one" n
1.22    "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
1.23    "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
1.24 @@ -44,7 +44,7 @@
1.25    appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b"
1.26    "appl p = (let (f, x) = p in f x)"
1.27
1.28 -code_generate (ml) Pair fst snd Let split swap swapp appl
1.29 +code_generate (ml, haskell) Pair fst snd Let split swap swapp appl
1.30
1.31  definition
1.32    k :: "int"
1.33 @@ -56,7 +56,7 @@
1.34  recdef fac "measure nat"
1.35    "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))"
1.36
1.37 -code_generate (ml)
1.39    "0::int" k
1.40    "op + :: int \<Rightarrow> int \<Rightarrow> int"
1.41    "op - :: int \<Rightarrow> int \<Rightarrow> int"
1.42 @@ -67,11 +67,11 @@
1.43
1.44  subsection {* sums *}
1.45
1.46 -code_generate (ml) Inl Inr
1.47 +code_generate (ml, haskell) Inl Inr
1.48
1.49  subsection {* options *}
1.50
1.51 -code_generate (ml) None Some
1.52 +code_generate (ml, haskell) None Some
1.53
1.54  subsection {* lists *}
1.55
1.56 @@ -81,7 +81,7 @@
1.57    qs :: "nat list"
1.58    "qs == rev ps"
1.59
1.60 -code_generate (ml) hd tl "op @" ps qs
1.61 +code_generate (ml, haskell) hd tl "op @" ps qs
1.62
1.63  subsection {* mutual datatypes *}
1.64
1.65 @@ -98,11 +98,11 @@
1.66    "mut2 mut2.Tip = mut2.Tip"
1.67    "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
1.68
1.69 -code_generate (ml) mut1 mut2
1.70 +code_generate (ml, haskell) mut1 mut2
1.71
1.72  subsection {* equalities *}
1.73
1.74 -code_generate (ml)