--- 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"