equal
deleted
inserted
replaced
48 "insert x (- set xs) = - set (removeAll x xs)" |
48 "insert x (- set xs) = - set (removeAll x xs)" |
49 by auto |
49 by auto |
50 |
50 |
51 lemma remove_set_compl: |
51 lemma remove_set_compl: |
52 "remove x (- set xs) = - set (List.insert x xs)" |
52 "remove x (- set xs) = - set (List.insert x xs)" |
53 by (auto simp del: mem_def simp add: remove_def List.insert_def) |
53 by (auto simp add: remove_def List.insert_def) |
54 |
54 |
55 lemma image_set: |
55 lemma image_set: |
56 "image f (set xs) = set (map f xs)" |
56 "image f (set xs) = set (map f xs)" |
57 by simp |
57 by simp |
58 |
58 |