src/HOL/Induct/Perm.thy

--- a/src/HOL/Induct/Perm.thy	Wed Mar 08 16:14:12 2000 +0100
+++ b/src/HOL/Induct/Perm.thy	Wed Mar 08 16:15:41 2000 +0100
@@ -21,4 +21,12 @@
     Cons  "xs <~~> ys ==> z#xs <~~> z#ys"
     trans "[| xs <~~> ys;  ys <~~> zs |] ==> xs <~~> zs"
 
+
+consts
+  remove  :: ['a, 'a list] => 'a list
+
+primrec 
+  "remove x []     = []"
+  "remove x (y#ys) = (if x=y then ys else y#remove x ys)"
+
 end