1.1 --- a/src/HOL/Library/Permutation.thy	Fri Nov 06 21:53:20 2009 +0100
     1.2 +++ b/src/HOL/Library/Permutation.thy	Sat Nov 07 08:18:12 2009 +0100
     1.3 @@ -93,11 +93,9 @@
     1.4  
     1.5  subsection {* Removing elements *}
     1.6  
     1.7 -consts
     1.8 -  remove :: "'a => 'a list => 'a list"
     1.9 -primrec
    1.10 -  "remove x [] = []"
    1.11 -  "remove x (y # ys) = (if x = y then ys else y # remove x ys)"
    1.12 +primrec remove :: "'a => 'a list => 'a list" where
    1.13 +    "remove x [] = []"
    1.14 +  | "remove x (y # ys) = (if x = y then ys else y # remove x ys)"
    1.15  
    1.16  lemma perm_remove: "x \<in> set ys ==> ys <~~> x # remove x ys"
    1.17    by (induct ys) auto
    1.18 @@ -156,7 +154,7 @@
    1.19    done
    1.20  
    1.21  lemma multiset_of_le_perm_append:
    1.22 -    "(multiset_of xs \<le># multiset_of ys) = (\<exists>zs. xs @ zs <~~> ys)";
    1.23 +    "(multiset_of xs \<le># multiset_of ys) = (\<exists>zs. xs @ zs <~~> ys)"
    1.24    apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv)
    1.25    apply (insert surj_multiset_of, drule surjD)
    1.26    apply (blast intro: sym)+

     2.1 --- a/src/HOL/Library/Sublist_Order.thy	Fri Nov 06 21:53:20 2009 +0100
     2.2 +++ b/src/HOL/Library/Sublist_Order.thy	Sat Nov 07 08:18:12 2009 +0100
     2.3 @@ -226,8 +226,7 @@
     2.4  lemma le_list_filter: "xs \<le> ys \<Longrightarrow> filter f xs \<le> filter f ys"
     2.5  by (induct rule: less_eq_list.induct) (auto intro: less_eq_list.drop)
     2.6  
     2.7 -
     2.8 -lemma "xs <= ys \<longleftrightarrow> (EX N. xs = sublist ys N)" (is "?L = ?R")
     2.9 +lemma "xs \<le> ys \<longleftrightarrow> (EX N. xs = sublist ys N)" (is "?L = ?R")
    2.10  proof
    2.11    assume ?L
    2.12    thus ?R

     3.1 --- a/src/HOL/ex/Codegenerator_Candidates.thy	Fri Nov 06 21:53:20 2009 +0100
     3.2 +++ b/src/HOL/ex/Codegenerator_Candidates.thy	Sat Nov 07 08:18:12 2009 +0100
     3.3 @@ -25,6 +25,13 @@
     3.4    "~~/src/HOL/ex/Records"
     3.5  begin
     3.6  
     3.7 +inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
     3.8 +    empty: "sublist [] xs"
     3.9 +  | drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
    3.10 +  | take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
    3.11 +
    3.12 +code_pred sublist .
    3.13 +
    3.14  (*avoid popular infix*)
    3.15  code_reserved SML upto
    3.16