--- a/src/HOL/Codegenerator_Test/Candidates.thy Tue Oct 21 17:23:16 2014 +0200
+++ b/src/HOL/Codegenerator_Test/Candidates.thy Tue Oct 21 21:10:44 2014 +0200
@@ -12,11 +12,6 @@
"~~/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"