src/HOL/List.ML

 goal List.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 qed "mem_filter";
 
-(** setOfList **)
-
-goal thy "setOfList (xs@ys) = (setOfList xs Un setOfList ys)";
-by (list.induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-by (Fast_tac 1);
-qed "setOfList_append";
-
-goal thy "(x mem xs) = (x: setOfList xs)";
-by (list.induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
-by (Fast_tac 1);
-qed "setOfList_mem_eq";
+(** set_of_list **)
+
+goal thy "set_of_list (xs@ys) = (set_of_list xs Un set_of_list ys)";
+by (list.induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+by (Fast_tac 1);
+qed "set_of_list_append";
+
+goal thy "(x mem xs) = (x: set_of_list xs)";
+by (list.induct_tac "xs" 1);
+by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+by (Fast_tac 1);
+qed "set_of_list_mem_eq";
 
 
 (** list_all **)
 
 goal List.thy "(Alls x:xs.True) = True";