# HG changeset patch
# User haftmann
# Date 1169713957 -3600
# Node ID 29b95968272b68e1441c092b6fa2ff83bf00ca05
# Parent  515021e98684dba8086914d2236fa97e107dd645
made executable

diff -r 515021e98684 -r 29b95968272b src/HOL/Library/List_Prefix.thy
--- a/src/HOL/Library/List_Prefix.thy	Thu Jan 25 09:32:36 2007 +0100
+++ b/src/HOL/Library/List_Prefix.thy	Thu Jan 25 09:32:37 2007 +0100
@@ -280,4 +280,21 @@
   then show "xs >>= ys" ..
 qed
 
+
+subsection {* Exeuctable code *}
+
+lemma less_eq_code [code func]:
+  "([]\<Colon>'a\<Colon>{eq, ord} list) \<le> xs \<longleftrightarrow> True"
+  "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> [] \<longleftrightarrow> False"
+  "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
+  by simp_all
+
+lemma less_code [code func]:
+  "xs < ([]\<Colon>'a\<Colon>{eq, ord} list) \<longleftrightarrow> False"
+  "[] < (x\<Colon>'a\<Colon>{eq, ord})# xs \<longleftrightarrow> True"
+  "(x\<Colon>'a\<Colon>{eq, ord}) # xs < y # ys \<longleftrightarrow> x = y \<and> xs < ys"
+  unfolding strict_prefix_def by auto
+
+lemmas [code func] = postfix_to_prefix
+
 end