author | haftmann |
Thu, 21 May 2020 20:00:08 +0000 | |
changeset 71853 | 30d92e668b52 |
parent 71852 | 76784f47c60f |
child 71854 | 6a51e64ba13d |
--- 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