src/HOL/List.ML
changeset 1936 979e8b4f5fa5
parent 1908 55d8e38262a8
child 1985 84cf16192e03
equal deleted inserted replaced
1935:ec67a0507c2a 1936:979e8b4f5fa5
    91 goal thy "(x mem xs) = (x: set_of_list xs)";
    91 goal thy "(x mem xs) = (x: set_of_list xs)";
    92 by (list.induct_tac "xs" 1);
    92 by (list.induct_tac "xs" 1);
    93 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
    93 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
    94 by (Fast_tac 1);
    94 by (Fast_tac 1);
    95 qed "set_of_list_mem_eq";
    95 qed "set_of_list_mem_eq";
       
    96 
       
    97 goal List.thy "set_of_list l <= set_of_list (x#l)";
       
    98 by (Simp_tac 1);
       
    99 by (Fast_tac 1);
       
   100 qed "set_of_list_subset_Cons";
    96 
   101 
    97 
   102 
    98 (** list_all **)
   103 (** list_all **)
    99 
   104 
   100 goal List.thy "(Alls x:xs.True) = True";
   105 goal List.thy "(Alls x:xs.True) = True";