# HG changeset patch
# User haftmann
# Date 1257578273 -3600
# Node ID 22e5725be1f303e8eee9dfa4c8a9d45ff961338f
# Parent  30e6e070bdb6b12549c326bb83e1d638a6723ea9
added predicate example

diff -r 30e6e070bdb6 -r 22e5725be1f3 src/HOL/ex/Codegenerator_Candidates.thy
--- 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