# HG changeset patch
# User haftmann
# Date 1590091208 0
# Node ID 30d92e668b52113422e3f8cfa7c7c9bdbabe0bfd
# Parent  76784f47c60f6562e91c19adb1a502738ea264b9
tuned module name space for generated code

diff -r 76784f47c60f -r 30d92e668b52 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Thu May 21 22:06:15 2020 +0200
+++ b/src/HOL/Parity.thy	Thu May 21 20:00:08 2020 +0000
@@ -1668,4 +1668,7 @@
   \<open>drop_bit n k < 0 \<longleftrightarrow> k < 0\<close> for k :: int
   by (subst Not_eq_iff [symmetric]) (simp add: not_less)
 
+code_identifier
+  code_module Parity \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
+
 end