src/HOL/ex/Codegenerator_Pretty.thy
author haftmann
Fri Jan 25 14:53:56 2008 +0100 (2008-01-25)
changeset 25963 07e08dad8a77
parent 25933 7fc0f4065251
child 26022 b30a342a6e29
permissions -rw-r--r--
distinguished examples for Efficient_Nat.thy
haftmann@24195
     1
(*  Title:      HOL/ex/Codegenerator_Pretty.thy
haftmann@24195
     2
    ID:         $Id$
haftmann@24195
     3
    Author:     Florian Haftmann, TU Muenchen
haftmann@24195
     4
*)
haftmann@24195
     5
haftmann@24195
     6
header {* Simple examples for pretty numerals and such *}
haftmann@24195
     7
haftmann@24195
     8
theory Codegenerator_Pretty
haftmann@25963
     9
imports ExecutableContent Code_Char Efficient_Nat
haftmann@24195
    10
begin
haftmann@24195
    11
haftmann@25963
    12
declare term_of_index.simps [code func del]
haftmann@25933
    13
haftmann@25963
    14
declare char.recs [code func del]
haftmann@25963
    15
  char.cases [code func del]
haftmann@25963
    16
  char.size [code func del]
haftmann@25963
    17
  term_of_char.simps [code func del]
haftmann@24195
    18
haftmann@25963
    19
declare isnorm.simps [code func del]
haftmann@25933
    20
haftmann@25963
    21
ML {* (*FIXME get rid of this*)
haftmann@25963
    22
nonfix union;
haftmann@25963
    23
nonfix inter;
haftmann@25963
    24
nonfix upto;
haftmann@25963
    25
*}
haftmann@25933
    26
haftmann@25963
    27
export_code * in SML module_name CodegenTest
haftmann@25963
    28
  in OCaml module_name CodegenTest file -
haftmann@25963
    29
  in Haskell file -
haftmann@25616
    30
haftmann@25963
    31
ML {*
haftmann@25963
    32
infix union;
haftmann@25963
    33
infix inter;
haftmann@25963
    34
infix 4 upto;
haftmann@25963
    35
*}
haftmann@24195
    36
haftmann@24195
    37
end