equal
deleted
inserted
replaced
|
1 (* Title: Pure/Tools/codegen_package.ML |
|
2 ID: $Id$ |
|
3 Author: Florian Haftmann, TU Muenchen |
|
4 |
|
5 Code extractor from Isabelle theories to |
|
6 intermediate language ("Thin-gol"). |
|
7 *) |
|
8 |
|
9 (*NOTE: for simpliying development, this package contains |
|
10 some stuff which will finally be moved upwards to HOL*) |
|
11 |
|
12 signature CODEGEN_PACKAGE = |
|
13 sig |
|
14 val bot: unit; |
|
15 end; |
|
16 |
|
17 structure CodegenPackage: CODEGEN_PACKAGE = |
|
18 struct |
|
19 |
|
20 val bot = (); |
|
21 |
|
22 end; (* structure *) |