diff -r 19e8b730ddeb -r 71e84a203c19 src/HOL/Codegenerator_Test/Candidates.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/Candidates.thy	Fri Jul 02 14:23:18 2010 +0200
@@ -0,0 +1,25 @@
+
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* A huge collection of equations to generate code from *}
+
+theory Candidates
+imports
+  Complex_Main
+  Library
+  List_Prefix
+  "~~/src/HOL/Number_Theory/Primes"
+  "~~/src/HOL/ex/Records"
+begin
+
+inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
+    empty: "sublist [] xs"
+  | drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
+  | take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
+
+code_pred sublist .
+
+(*avoid popular infix*)
+code_reserved SML upto
+
+end