src/HOL/List.thy

--- a/src/HOL/List.thy	Mon Sep 21 22:58:43 1998 +0200
+++ b/src/HOL/List.thy	Mon Sep 21 23:03:11 1998 +0200
@@ -17,7 +17,9 @@
   foldl       :: [['b,'a] => 'b, 'b, 'a list] => 'b
   hd, last    :: 'a list => 'a
   set         :: 'a list => 'a set
+  list_all    :: ('a => bool) => ('a list => bool)
   map         :: ('a=>'b) => ('a list => 'b list)
+  mem         :: ['a, 'a list] => bool                    (infixl 55)
   nth         :: ['a list, nat] => 'a			  (infixl "!" 100)
   list_update :: 'a list => nat => 'a => 'a list
   take, drop  :: [nat, 'a list] => 'a list
@@ -35,9 +37,6 @@
   lupdbinds  lupdbind
 
 syntax
-  mem         :: ['a, 'a list] => bool                    (infixl 55)
-  list_all    :: ('a => bool) => ('a list => bool)
-
   (* list Enumeration *)
   "@list"     :: args => 'a list                          ("[(_)]")
 
@@ -53,9 +52,6 @@
   upto        :: nat => nat => nat list                   ("(1[_../_])")
 
 translations
-  "x mem xs"      == "x:set xs"
-  "list_all P xs" == "Ball (set xs) P"
-  
   "[x, xs]"     == "x#[xs]"
   "[x]"         == "x#[]"
   "[x:xs . P]"  == "filter (%x. P) xs"
@@ -97,9 +93,15 @@
   "butlast [] = []"
   "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
 primrec
+  "x mem [] = False"
+  "x mem (y#ys) = (if y=x then True else x mem ys)"
+primrec
   "set [] = {}"
   "set (x#xs) = insert x (set xs)"
 primrec
+  list_all_Nil  "list_all P [] = True"
+  list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"
+primrec
   "map f [] = []"
   "map f (x#xs) = f(x)#map f xs"
 primrec