# 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]: + "([]\'a\{eq, ord} list) \ xs \ True" + "(x\'a\{eq, ord}) # xs \ [] \ False" + "(x\'a\{eq, ord}) # xs \ y # ys \ x = y \ xs \ ys" + by simp_all + +lemma less_code [code func]: + "xs < ([]\'a\{eq, ord} list) \ False" + "[] < (x\'a\{eq, ord})# xs \ True" + "(x\'a\{eq, ord}) # xs < y # ys \ x = y \ xs < ys" + unfolding strict_prefix_def by auto + +lemmas [code func] = postfix_to_prefix + end