| changeset 50630 | 1ea90e8046dc |
| parent 48430 | 6cbfe187a0f9 |
| child 51143 | 0a2371e7ced3 |
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Fri Dec 28 10:15:39 2012 +0100 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Fri Dec 28 10:25:59 2012 +0100 @@ -1000,7 +1000,7 @@ ML {* @{code test_2} () *} ML {* @{code test_3} () *} -export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp? +export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp end