| changeset 38058 | e4640c2ceb43 |
| parent 37966 | ac9bcae5ada7 |
| child 38068 | 00042fd999a8 |
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Thu Jul 29 09:56:59 2010 +0200 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Thu Jul 29 09:56:59 2010 +0200 @@ -1014,6 +1014,6 @@ 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? +export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? (*Scala_imp?*) end