changeset 33364 | 2bd12592c5e8 |
parent 33319 | 74f0dcc0b5fb |
child 33676 | 802f5e233e48 |
--- a/src/HOL/Ring_and_Field.thy Fri Oct 30 14:02:42 2009 +0100 +++ b/src/HOL/Ring_and_Field.thy Fri Oct 30 18:32:40 2009 +0100 @@ -2374,4 +2374,14 @@ then show ?thesis by simp qed + +code_modulename SML + Ring_and_Field Arith + +code_modulename OCaml + Ring_and_Field Arith + +code_modulename Haskell + Ring_and_Field Arith + end