diff -r 74a81d6f3c54 -r 398e05aa84d4 src/HOL/Codegenerator_Test/Candidates.thy
--- a/src/HOL/Codegenerator_Test/Candidates.thy	Tue Oct 14 16:19:42 2014 +0200
+++ b/src/HOL/Codegenerator_Test/Candidates.thy	Tue Oct 14 08:23:23 2014 +0200
@@ -12,6 +12,11 @@
   "~~/src/HOL/ex/Records"
 begin
 
+lemma [code]: -- {* Formal joining of hierarchy of implicit definitions in Scala *}
+  fixes a :: "'a :: semiring_div_parity"
+  shows "even a \<longleftrightarrow> a mod 2 = 0"
+  by (fact even_iff_mod_2_eq_zero)
+
 inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
 where
   empty: "sublist [] xs"