equal
deleted
inserted
replaced
1 (* Title: HOL/Library/Code_Test.thy |
1 (* Title: HOL/Library/Code_Test.thy |
2 Author: Andreas Lochbihler, ETH Zürich |
2 Author: Andreas Lochbihler, ETH Zürich |
3 |
3 |
4 Test infrastructure for the code generator. |
4 Test infrastructure for the code generator. |
5 *) |
5 *) |
|
6 |
|
7 section \<open>Test infrastructure for the code generator\<close> |
6 |
8 |
7 theory Code_Test |
9 theory Code_Test |
8 imports Main |
10 imports Main |
9 keywords "test_code" :: diag |
11 keywords "test_code" :: diag |
10 begin |
12 begin |