equal
deleted
inserted
replaced
|
1 |
|
2 (* Author: Florian Haftmann, TU Muenchen *) |
|
3 |
|
4 header {* A huge collection of equations to generate code from *} |
|
5 |
|
6 theory Codegenerator_Candidates |
|
7 imports |
|
8 Complex_Main |
|
9 AssocList |
|
10 Binomial |
|
11 Commutative_Ring |
|
12 Enum |
|
13 List_Prefix |
|
14 Nat_Infinity |
|
15 Nested_Environment |
|
16 Option_ord |
|
17 Permutation |
|
18 Primes |
|
19 Product_ord |
|
20 SetsAndFunctions |
|
21 While_Combinator |
|
22 Word |
|
23 "~~/src/HOL/ex/Commutative_Ring_Complete" |
|
24 "~~/src/HOL/ex/Records" |
|
25 begin |
|
26 |
|
27 (*temporary Haskell workaround*) |
|
28 declare typerep_fun_def [code inline] |
|
29 declare typerep_prod_def [code inline] |
|
30 declare typerep_sum_def [code inline] |
|
31 declare typerep_cpoint_ext_type_def [code inline] |
|
32 declare typerep_itself_def [code inline] |
|
33 declare typerep_list_def [code inline] |
|
34 declare typerep_option_def [code inline] |
|
35 declare typerep_point_ext_type_def [code inline] |
|
36 declare typerep_point'_ext_type_def [code inline] |
|
37 declare typerep_point''_ext_type_def [code inline] |
|
38 declare typerep_pol_def [code inline] |
|
39 declare typerep_polex_def [code inline] |
|
40 |
|
41 (*avoid popular infixes*) |
|
42 code_reserved SML union inter upto |
|
43 |
|
44 end |