# 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 \<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)+