--- a/src/HOL/ex/Codegenerator_Candidates.thy Sat Nov 07 08:17:52 2009 +0100
+++ b/src/HOL/ex/Codegenerator_Candidates.thy Sat Nov 07 08:17:53 2009 +0100
@@ -25,6 +25,13 @@
"~~/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