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 \<longleftrightarrow> #4 * #2 + #7 = (#8 :: nat) \<and> #4 * #2 + #7 \<ge> (#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