src/HOL/ex/Codegenerator_Pretty.thy
author haftmann
Mon, 16 Feb 2009 13:38:09 +0100
changeset 29933 125d513d9e39
parent 28663 bd8438543bf2
child 31378 d1cbf6393964
permissions -rw-r--r--
dropped Id
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24195
haftmann
parents:
diff changeset
     1
(*  Title:      HOL/ex/Codegenerator_Pretty.thy
haftmann
parents:
diff changeset
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann
parents:
diff changeset
     3
*)
haftmann
parents:
diff changeset
     4
haftmann
parents:
diff changeset
     5
header {* Simple examples for pretty numerals and such *}
haftmann
parents:
diff changeset
     6
haftmann
parents:
diff changeset
     7
theory Codegenerator_Pretty
25963
07e08dad8a77 distinguished examples for Efficient_Nat.thy
haftmann
parents: 25933
diff changeset
     8
imports ExecutableContent Code_Char Efficient_Nat
24195
haftmann
parents:
diff changeset
     9
begin
haftmann
parents:
diff changeset
    10
28562
4e74209f113e `code func` now just `code`
haftmann
parents: 28335
diff changeset
    11
declare isnorm.simps [code del]
28228
7ebe8dc06cbb evaluation using code generator
haftmann
parents: 26468
diff changeset
    12
25963
07e08dad8a77 distinguished examples for Efficient_Nat.thy
haftmann
parents: 25933
diff changeset
    13
ML {* (*FIXME get rid of this*)
07e08dad8a77 distinguished examples for Efficient_Nat.thy
haftmann
parents: 25933
diff changeset
    14
nonfix union;
07e08dad8a77 distinguished examples for Efficient_Nat.thy
haftmann
parents: 25933
diff changeset
    15
nonfix inter;
07e08dad8a77 distinguished examples for Efficient_Nat.thy
haftmann
parents: 25933
diff changeset
    16
nonfix upto;
07e08dad8a77 distinguished examples for Efficient_Nat.thy
haftmann
parents: 25933
diff changeset
    17
*}
25933
7fc0f4065251 proper meaningful examples
haftmann
parents: 25616
diff changeset
    18
25963
07e08dad8a77 distinguished examples for Efficient_Nat.thy
haftmann
parents: 25933
diff changeset
    19
export_code * in SML module_name CodegenTest
07e08dad8a77 distinguished examples for Efficient_Nat.thy
haftmann
parents: 25933
diff changeset
    20
  in OCaml module_name CodegenTest file -
07e08dad8a77 distinguished examples for Efficient_Nat.thy
haftmann
parents: 25933
diff changeset
    21
  in Haskell file -
25616
28d373f1482a added div/mod examples
haftmann
parents: 24530
diff changeset
    22
25963
07e08dad8a77 distinguished examples for Efficient_Nat.thy
haftmann
parents: 25933
diff changeset
    23
ML {*
07e08dad8a77 distinguished examples for Efficient_Nat.thy
haftmann
parents: 25933
diff changeset
    24
infix union;
07e08dad8a77 distinguished examples for Efficient_Nat.thy
haftmann
parents: 25933
diff changeset
    25
infix inter;
07e08dad8a77 distinguished examples for Efficient_Nat.thy
haftmann
parents: 25933
diff changeset
    26
infix 4 upto;
07e08dad8a77 distinguished examples for Efficient_Nat.thy
haftmann
parents: 25933
diff changeset
    27
*}
24195
haftmann
parents:
diff changeset
    28
haftmann
parents:
diff changeset
    29
end