tuned module name space for generated code
authorhaftmann
Thu May 21 20:00:08 2020 +0000 (10 days ago)
changeset 7185330d92e668b52
parent 71852 76784f47c60f
child 71854 6a51e64ba13d
tuned module name space for generated code
src/HOL/Parity.thy
     1.1 --- a/src/HOL/Parity.thy	Thu May 21 22:06:15 2020 +0200
     1.2 +++ b/src/HOL/Parity.thy	Thu May 21 20:00:08 2020 +0000
     1.3 @@ -1668,4 +1668,7 @@
     1.4    \<open>drop_bit n k < 0 \<longleftrightarrow> k < 0\<close> for k :: int
     1.5    by (subst Not_eq_iff [symmetric]) (simp add: not_less)
     1.6  
     1.7 +code_identifier
     1.8 +  code_module Parity \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
     1.9 +
    1.10  end