src/HOL/Imperative_HOL/ex/Linked_Lists.thy
changeset 37826 4c0a5e35931a
parent 37792 ba0bc31b90d7
child 37828 9e1758c7ff06
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Wed Jul 14 16:02:50 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Wed Jul 14 16:13:14 2010 +0200
@@ -991,10 +991,6 @@
 
 section {* Code generation *}
 
-export_code merge in SML file -
-
-export_code rev in SML file -
-
 text {* A simple example program *}
 
 definition test_1 where "test_1 = (do { ll_xs <- make_llist [1..(15::int)]; xs <- traverse ll_xs; return xs })" 
@@ -1018,9 +1014,6 @@
 ML {* @{code test_2} () *}
 ML {* @{code test_3} () *}
 
-export_code test_1 test_2 test_3 in SML_imp module_name QSort file -
-export_code test_1 test_2 test_3 in OCaml module_name QSort file -
-export_code test_1 test_2 test_3 in OCaml_imp module_name QSort file -
-export_code test_1 test_2 test_3 in Haskell module_name QSort file -
+export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell?
 
 end