src/HOL/ex/Codegenerator_Pretty_Test.thy
author haftmann
Wed, 13 Jan 2010 08:56:16 +0100
changeset 34887 31209fb24176
parent 34306 e8b8ee60c1e2
child 37475 98c6f9dc58d0
permissions -rw-r--r--
deactivate pretty code test for Scala -- no proper setup yet
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31378
d1cbf6393964 tuned code generator test theories
haftmann
parents: 29933
diff changeset
     1
d1cbf6393964 tuned code generator test theories
haftmann
parents: 29933
diff changeset
     2
(* Author: Florian Haftmann, TU Muenchen *)
24195
haftmann
parents:
diff changeset
     3
31378
d1cbf6393964 tuned code generator test theories
haftmann
parents: 29933
diff changeset
     4
header {* Pervasive test of code generator using pretty literals *}
24195
haftmann
parents:
diff changeset
     5
31378
d1cbf6393964 tuned code generator test theories
haftmann
parents: 29933
diff changeset
     6
theory Codegenerator_Pretty_Test
d1cbf6393964 tuned code generator test theories
haftmann
parents: 29933
diff changeset
     7
imports Codegenerator_Pretty
24195
haftmann
parents:
diff changeset
     8
begin
haftmann
parents:
diff changeset
     9
25963
07e08dad8a77 distinguished examples for Efficient_Nat.thy
haftmann
parents: 25933
diff changeset
    10
export_code * in SML module_name CodegenTest
07e08dad8a77 distinguished examples for Efficient_Nat.thy
haftmann
parents: 25933
diff changeset
    11
  in OCaml module_name CodegenTest file -
07e08dad8a77 distinguished examples for Efficient_Nat.thy
haftmann
parents: 25933
diff changeset
    12
  in Haskell file -
34887
31209fb24176 deactivate pretty code test for Scala -- no proper setup yet
haftmann
parents: 34306
diff changeset
    13
(*in Scala file -*)
25616
28d373f1482a added div/mod examples
haftmann
parents: 24530
diff changeset
    14
24195
haftmann
parents:
diff changeset
    15
end