equal
deleted
inserted
replaced
2569 declare atom_eqvt[eqvt] |
2569 declare atom_eqvt[eqvt] |
2570 |
2570 |
2571 class at = at_base + |
2571 class at = at_base + |
2572 assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)" |
2572 assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)" |
2573 |
2573 |
|
2574 lemma sort_ineq [simp]: |
|
2575 assumes "sort_of (atom a) \<noteq> sort_of (atom b)" |
|
2576 shows "atom a \<noteq> atom b" |
|
2577 using assms by metis |
|
2578 |
2574 lemma supp_at_base: |
2579 lemma supp_at_base: |
2575 fixes a::"'a::at_base" |
2580 fixes a::"'a::at_base" |
2576 shows "supp a = {atom a}" |
2581 shows "supp a = {atom a}" |
2577 by (simp add: supp_atom [symmetric] supp_def atom_eqvt) |
2582 by (simp add: supp_atom [symmetric] supp_def atom_eqvt) |
2578 |
2583 |