changeset 66453 | cc19f7ca2ed6 |
parent 65552 | f533820e7248 |
child 68155 | 8b50f29a1992 |
--- a/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy Fri Aug 18 13:55:05 2017 +0200 +++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy Fri Aug 18 20:47:47 2017 +0200 @@ -4,7 +4,7 @@ Test case for test_code on OCaml *) -theory Code_Test_OCaml imports "../Library/Code_Test" begin +theory Code_Test_OCaml imports "HOL-Library.Code_Test" begin test_code "14 + 7 * -12 = (140 div -2 :: integer)" in OCaml