src/HOL/Imperative_HOL/ex/Linked_Lists.thy
changeset 38068 00042fd999a8
parent 38058 e4640c2ceb43
child 38410 8e4058f4848c
equal deleted inserted replaced
38060:a9b52497661c 38068:00042fd999a8
  1012 
  1012 
  1013 ML {* @{code test_1} () *}
  1013 ML {* @{code test_1} () *}
  1014 ML {* @{code test_2} () *}
  1014 ML {* @{code test_2} () *}
  1015 ML {* @{code test_3} () *}
  1015 ML {* @{code test_3} () *}
  1016 
  1016 
  1017 export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? (*Scala_imp?*)
  1017 export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp?
  1018 
  1018 
  1019 end
  1019 end