equal
deleted
inserted
replaced
7 atom_decl tvar var |
7 atom_decl tvar var |
8 |
8 |
9 abbreviation |
9 abbreviation |
10 "difference_list" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" ("_ - _" [60,60] 60) |
10 "difference_list" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" ("_ - _" [60,60] 60) |
11 where |
11 where |
12 "xs - ys \<equiv> [x \<leftarrow> xs. x\<notin>set ys]" |
12 "xs - ys \<equiv> filter (\<lambda>x. x\<notin>set ys) xs" |
13 |
13 |
14 lemma difference_eqvt_tvar[eqvt]: |
14 lemma difference_eqvt_tvar[eqvt]: |
15 fixes pi::"tvar prm" |
15 fixes pi::"tvar prm" |
16 and Xs Ys::"tvar list" |
16 and Xs Ys::"tvar list" |
17 shows "pi\<bullet>(Xs - Ys) = (pi\<bullet>Xs) - (pi\<bullet>Ys)" |
17 shows "pi\<bullet>(Xs - Ys) = (pi\<bullet>Xs) - (pi\<bullet>Ys)" |