# HG changeset patch # User haftmann # Date 1257578272 -3600 # Node ID 318acc1c9399eeddb4649f716df90b3467a43a8f # Parent 0183f9545fa2b225e6d30aaddbc6690d7fb8ad2a modernized primrec diff -r 0183f9545fa2 -r 318acc1c9399 src/HOL/Library/Permutation.thy --- a/src/HOL/Library/Permutation.thy Fri Nov 06 13:42:29 2009 +0100 +++ b/src/HOL/Library/Permutation.thy Sat Nov 07 08:17:52 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 \ 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 \# multiset_of ys) = (\zs. xs @ zs <~~> ys)"; + "(multiset_of xs \# multiset_of ys) = (\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)+