equal
deleted
inserted
replaced
1 theory Abs |
1 theory Abs |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "../QuotProd" |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product" |
3 begin |
3 begin |
4 |
4 |
5 (* the next three lemmas that should be in Nominal \<dots>\<dots>must be cleaned *) |
5 (* the next three lemmas that should be in Nominal \<dots>\<dots>must be cleaned *) |
6 lemma ball_image: |
6 lemma ball_image: |
7 shows "(\<forall>x \<in> p \<bullet> S. P x) = (\<forall>x \<in> S. P (p \<bullet> x))" |
7 shows "(\<forall>x \<in> p \<bullet> S. P x) = (\<forall>x \<in> S. P (p \<bullet> x))" |