# HG changeset patch
# User paulson
# Date 835023071 -7200
# Node ID 785a7672962e36274710f435a46b7369747df62c
# Parent  3ff66483a8d4b50327ad3281374d5349ffcc2839
Removed quantification over lists

diff -r 3ff66483a8d4 -r 785a7672962e src/HOL/ex/SList.ML
--- a/src/HOL/ex/SList.ML	Mon Jun 17 16:50:38 1996 +0200
+++ b/src/HOL/ex/SList.ML	Mon Jun 17 16:51:11 1996 +0200
@@ -286,7 +286,6 @@
 val [map_Nil,map_Cons] = list_recs map_def;
 val [list_case_Nil,list_case_Cons] = list_recs list_case_def;
 val [filter_Nil,filter_Cons] = list_recs filter_def;
-val [list_all_Nil,list_all_Cons] = list_recs list_all_def;
 
 Addsimps
   [null_Nil, ttl_Nil,
@@ -294,7 +293,6 @@
    list_case_Nil, list_case_Cons,
    append_Nil3, append_Cons,
    map_Nil, map_Cons,
-   list_all_Nil, list_all_Cons,
    filter_Nil, filter_Cons];
 
 
@@ -322,24 +320,6 @@
 by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 qed "mem_filter2";
 
-(** list_all **)
-
-goal SList.thy "(Alls x:xs.True) = True";
-by(list_ind_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
-qed "list_all_True2";
-
-goal SList.thy "list_all p (xs@ys) = (list_all p xs & list_all p ys)";
-by(list_ind_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
-qed "list_all_conj2";
-
-goal SList.thy "(Alls x:xs.P(x)) = (!x. x mem xs --> P(x))";
-by(list_ind_tac "xs" 1);
-by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
-by(fast_tac HOL_cs 1);
-qed "list_all_mem_conv2";
-
 
 (** The functional "map" **)
 
diff -r 3ff66483a8d4 -r 785a7672962e src/HOL/ex/SList.thy
--- a/src/HOL/ex/SList.thy	Mon Jun 17 16:50:38 1996 +0200
+++ b/src/HOL/ex/SList.thy	Mon Jun 17 16:51:11 1996 +0200
@@ -38,7 +38,6 @@
   hd        :: 'a list => 'a
   tl,ttl    :: 'a list => 'a list
   mem           :: ['a, 'a list] => bool                        (infixl 55)
-  list_all  :: ('a => bool) => ('a list => bool)
   map       :: ('a=>'b) => ('a list => 'b list)
   "@"       :: ['a list, 'a list] => 'a list                    (infixr 65)
   filter    :: ['a => bool, 'a list] => 'a list
@@ -48,8 +47,7 @@
   "[]"      :: 'a list                            ("[]")
   "@list"   :: args => 'a list                    ("[(_)]")
 
-  (* Special syntax for list_all and filter *)
-  "@Alls"       :: [idt, 'a list, bool] => bool ("(2Alls _:_./ _)" 10)
+  (* Special syntax for filter *)
   "@filter"     :: [idt, 'a list, bool] => 'a list      ("(1[_:_ ./ _])")
 
 translations
@@ -60,7 +58,6 @@
   "case xs of Nil => a | y#ys => b" == "list_case a (%y ys.b) xs"
 
   "[x:xs . P]"  == "filter (%x.P) xs"
-  "Alls x:xs.P" == "list_all (%x.P) xs"
 
 defs
   (* Defining the Concrete Constructors *)
@@ -109,7 +106,6 @@
 
   mem_def       "x mem xs            == 
                    list_rec xs False (%y ys r. if y=x then True else r)"
-  list_all_def  "list_all P xs       == list_rec xs True (%x l r. P(x) & r)"
   map_def       "map f xs            == list_rec xs [] (%x l r. f(x)#r)"
   append_def    "xs@ys               == list_rec xs ys (%x l r. x#r)"
   filter_def    "filter P xs         ==