equal
deleted
inserted
replaced
523 unfolding supp_Abs |
523 unfolding supp_Abs |
524 by auto |
524 by auto |
525 |
525 |
526 lemma Abs_fresh_star: |
526 lemma Abs_fresh_star: |
527 fixes x::"'a::fs" |
527 fixes x::"'a::fs" |
528 shows "as \<sharp>* Abs_set as x" |
528 shows "as \<subseteq> as' \<Longrightarrow> as \<sharp>* Abs_set as' x" |
529 and "as \<sharp>* Abs_res as x" |
529 and "as \<subseteq> as' \<Longrightarrow> as \<sharp>* Abs_res as' x" |
530 and "set bs \<sharp>* Abs_lst bs x" |
530 and "bs \<subseteq> set bs' \<Longrightarrow> bs \<sharp>* Abs_lst bs' x" |
531 unfolding fresh_star_def |
531 unfolding fresh_star_def |
532 by(simp_all add: Abs_fresh_iff) |
532 by(auto simp add: Abs_fresh_iff) |
533 |
533 |
534 |
534 |
535 section {* Infrastructure for building tuples of relations and functions *} |
535 section {* Infrastructure for building tuples of relations and functions *} |
536 |
536 |
537 fun |
537 fun |