| changeset 81713 | 378b9d6c52b2 |
| parent 81642 | e77e8ef5bf9b |
| child 81714 | 5e3dd01a9eb2 |
| 81712:97987036f051 | 81713:378b9d6c52b2 |
|---|---|
3 Author: Florian Haftmann, TU Muenchen |
3 Author: Florian Haftmann, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 theory Code_Test_OCaml |
6 theory Code_Test_OCaml |
7 imports |
7 imports |
8 "HOL-Library.Code_Target_Bit_Shifts" |
|
8 "HOL-Library.Code_Test" |
9 "HOL-Library.Code_Test" |
9 Code_Lazy_Test |
10 Code_Lazy_Test |
10 begin |
11 begin |
11 |
12 |
12 text \<open>Test cases for \<^text>\<open>test_code\<close>\<close> |
13 text \<open>Test cases for \<^text>\<open>test_code\<close>\<close> |