# HG changeset patch
# User haftmann
# Date 1257578292 -3600
# Node ID 31872dd275c89853d680f77ea426c9f30c7c45a6
# Parent  39c9d0785911b81235c9ff53f2ca5b158431db5f# Parent  22e5725be1f303e8eee9dfa4c8a9d45ff961338f
merged

diff -r 39c9d0785911 -r 31872dd275c8 src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Fri Nov 06 21:53:20 2009 +0100
+++ b/src/HOL/Library/Permutation.thy	Sat Nov 07 08:18:12 2009 +0100
@@ -93,11 +93,9 @@
 
 subsection {* Removing elements *}
 
-consts
-  remove :: "'a => 'a list => 'a list"
-primrec
-  "remove x [] = []"
-  "remove x (y # ys) = (if x = y then ys else y # remove x ys)"
+primrec remove :: "'a => 'a list => 'a list" where
+    "remove x [] = []"
+  | "remove x (y # ys) = (if x = y then ys else y # remove x ys)"
 
 lemma perm_remove: "x \<in> set ys ==> ys <~~> x # remove x ys"
   by (induct ys) auto
@@ -156,7 +154,7 @@
   done
 
 lemma multiset_of_le_perm_append:
-    "(multiset_of xs \<le># multiset_of ys) = (\<exists>zs. xs @ zs <~~> ys)";
+    "(multiset_of xs \<le># multiset_of ys) = (\<exists>zs. xs @ zs <~~> ys)"
   apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv)
   apply (insert surj_multiset_of, drule surjD)
   apply (blast intro: sym)+
diff -r 39c9d0785911 -r 31872dd275c8 src/HOL/Library/Sublist_Order.thy
--- a/src/HOL/Library/Sublist_Order.thy	Fri Nov 06 21:53:20 2009 +0100
+++ b/src/HOL/Library/Sublist_Order.thy	Sat Nov 07 08:18:12 2009 +0100
@@ -226,8 +226,7 @@
 lemma le_list_filter: "xs \<le> ys \<Longrightarrow> filter f xs \<le> filter f ys"
 by (induct rule: less_eq_list.induct) (auto intro: less_eq_list.drop)
 
-
-lemma "xs <= ys \<longleftrightarrow> (EX N. xs = sublist ys N)" (is "?L = ?R")
+lemma "xs \<le> ys \<longleftrightarrow> (EX N. xs = sublist ys N)" (is "?L = ?R")
 proof
   assume ?L
   thus ?R
diff -r 39c9d0785911 -r 31872dd275c8 src/HOL/ex/Codegenerator_Candidates.thy
--- a/src/HOL/ex/Codegenerator_Candidates.thy	Fri Nov 06 21:53:20 2009 +0100
+++ b/src/HOL/ex/Codegenerator_Candidates.thy	Sat Nov 07 08:18:12 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