# HG changeset patch # User haftmann # Date 1279116794 -7200 # Node ID 4c0a5e35931a18a7d75c1d82785341f7f1306258 # Parent adc1143bc1a8aa7f62d80a705ce548ed72fa2476 avoid export_code ... file - diff -r adc1143bc1a8 -r 4c0a5e35931a src/HOL/Imperative_HOL/Imperative_HOL_ex.thy --- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Wed Jul 14 16:02:50 2010 +0200 +++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Wed Jul 14 16:13:14 2010 +0200 @@ -10,4 +10,6 @@ "ex/Imperative_Quicksort" "ex/Imperative_Reverse" "ex/Linked_Lists" "ex/SatChecker" begin +export_code "Array.*" "Ref.*" checking SML SML_imp OCaml? OCaml_imp? Haskell? + end diff -r adc1143bc1a8 -r 4c0a5e35931a src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Wed Jul 14 16:02:50 2010 +0200 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Wed Jul 14 16:13:14 2010 +0200 @@ -655,9 +655,6 @@ ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *} -export_code qsort in SML_imp module_name QSort file - -export_code qsort in OCaml module_name QSort file - -export_code qsort in OCaml_imp module_name QSort file - -export_code qsort in Haskell module_name QSort file - +export_code qsort checking SML SML_imp OCaml? OCaml_imp? Haskell? end \ No newline at end of file diff -r adc1143bc1a8 -r 4c0a5e35931a src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy --- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Wed Jul 14 16:02:50 2010 +0200 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Wed Jul 14 16:13:14 2010 +0200 @@ -110,4 +110,6 @@ subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims) (drule sym[of "List.length (Array.get h a)"], simp) +export_code rev checking SML SML_imp OCaml? OCaml_imp? Haskell? + end diff -r adc1143bc1a8 -r 4c0a5e35931a src/HOL/Imperative_HOL/ex/Linked_Lists.thy --- 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 diff -r adc1143bc1a8 -r 4c0a5e35931a src/HOL/Imperative_HOL/ex/SatChecker.thy --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy Wed Jul 14 16:02:50 2010 +0200 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy Wed Jul 14 16:13:14 2010 +0200 @@ -710,8 +710,6 @@ code_const ProofDone and Root and Conflict and Delete and Xstep (SML "MinisatProofStep.ProofDone" and "MinisatProofStep.Root ((_),/ (_))" and "MinisatProofStep.Conflict ((_),/ (_))" and "MinisatProofStep.Delete" and "MinisatProofStep.Xstep ((_),/ (_))") -export_code checker in SML module_name SAT file - -export_code tchecker in SML module_name SAT file - -export_code lchecker in SML module_name SAT file - +export_code checker tchecker lchecker in SML end diff -r adc1143bc1a8 -r 4c0a5e35931a src/HOL/ex/Numeral.thy --- a/src/HOL/ex/Numeral.thy Wed Jul 14 16:02:50 2010 +0200 +++ b/src/HOL/ex/Numeral.thy Wed Jul 14 16:13:14 2010 +0200 @@ -988,9 +988,9 @@ subsection {* Toy examples *} definition "bar \ #4 * #2 + #7 = (#8 :: nat) \ #4 * #2 + #7 \ (#8 :: int) - #3" + code_thms bar -export_code bar in Haskell file - -export_code bar in OCaml module_name Foo file - -ML {* @{code bar} *} + +export_code bar checking SML OCaml? Haskell? end diff -r adc1143bc1a8 -r 4c0a5e35931a src/HOL/ex/Records.thy --- a/src/HOL/ex/Records.thy Wed Jul 14 16:02:50 2010 +0200 +++ b/src/HOL/ex/Records.thy Wed Jul 14 16:13:14 2010 +0200 @@ -346,6 +346,6 @@ subsection {* Some code generation *} -export_code foo1 foo3 foo5 foo10 foo11 in SML file - +export_code foo1 foo3 foo5 foo10 checking SML end