author haftmann Sat Nov 07 08:17:52 2009 +0100 (2009-11-07) changeset 33498 318acc1c9399 parent 33469 0183f9545fa2 child 33499 30e6e070bdb6
modernized primrec
```     1.1 --- a/src/HOL/Library/Permutation.thy	Fri Nov 06 13:42:29 2009 +0100
1.2 +++ b/src/HOL/Library/Permutation.thy	Sat Nov 07 08:17:52 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)+
```