equal
deleted
inserted
replaced
459 fixes a ::"'x" |
459 fixes a ::"'x" |
460 and b ::"'x" |
460 and b ::"'x" |
461 assumes a: "at TYPE('x)" |
461 assumes a: "at TYPE('x)" |
462 shows "[(a,b)]\<bullet>a = b" |
462 shows "[(a,b)]\<bullet>a = b" |
463 and "[(a,b)]\<bullet>b = a" |
463 and "[(a,b)]\<bullet>b = a" |
|
464 and "\<lbrakk>a\<noteq>c; b\<noteq>c\<rbrakk> \<Longrightarrow> [(a,b)]\<bullet>c = c" |
464 using a by (simp_all add: at_calc) |
465 using a by (simp_all add: at_calc) |
465 |
466 |
466 lemma at4: |
467 lemma at4: |
467 assumes a: "at TYPE('x)" |
468 assumes a: "at TYPE('x)" |
468 shows "infinite (UNIV::'x set)" |
469 shows "infinite (UNIV::'x set)" |