author | blanchet |
Fri, 01 Aug 2014 14:43:57 +0200 | |
changeset 57743 | 0af2d5dfb0ac |
parent 51161 | 6ed12ae3b3e1 |
child 58889 | 5b7a9633cfa8 |
permissions | -rw-r--r-- |
31378 | 1 |
|
2 |
(* Author: Florian Haftmann, TU Muenchen *) |
|
24195 | 3 |
|
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
4 |
header {* Pervasive test of code generator *} |
24195 | 5 |
|
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
6 |
theory Generate_Target_Nat |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
7 |
imports |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
8 |
Candidates |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
9 |
"~~/src/HOL/Library/AList_Mapping" |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
10 |
"~~/src/HOL/Library/Finite_Lattice" |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
11 |
"~~/src/HOL/Library/Code_Target_Numeral" |
24195 | 12 |
begin |
13 |
||
37745
6315b6426200
checking generated code for various target languages
haftmann
parents:
37695
diff
changeset
|
14 |
text {* |
37824 | 15 |
If any of the checks fails, inspect the code generated |
16 |
by a corresponding @{text export_code} command. |
|
37745
6315b6426200
checking generated code for various target languages
haftmann
parents:
37695
diff
changeset
|
17 |
*} |
6315b6426200
checking generated code for various target languages
haftmann
parents:
37695
diff
changeset
|
18 |
|
50629
264ece81df93
code checking for Scala is mandatory, since Scala is now required anyway for Isabelle
haftmann
parents:
47108
diff
changeset
|
19 |
export_code _ checking SML OCaml? Haskell? Scala |
25616 | 20 |
|
24195 | 21 |
end |