equal
deleted
inserted
replaced
1100 qed |
1100 qed |
1101 |
1101 |
1102 |
1102 |
1103 section {* Concrete atoms types *} |
1103 section {* Concrete atoms types *} |
1104 |
1104 |
|
1105 text {* |
|
1106 Class @{text at_base} allows types containing multiple sorts of atoms. |
|
1107 Class @{text at} only allows types with a single sort. |
|
1108 *} |
|
1109 |
1105 class at_base = pt + |
1110 class at_base = pt + |
1106 fixes atom :: "'a \<Rightarrow> atom" |
1111 fixes atom :: "'a \<Rightarrow> atom" |
1107 assumes atom_eq_iff [simp]: "atom a = atom b \<longleftrightarrow> a = b" |
1112 assumes atom_eq_iff [simp]: "atom a = atom b \<longleftrightarrow> a = b" |
1108 assumes atom_eqvt: "p \<bullet> (atom a) = atom (p \<bullet> a)" |
1113 assumes atom_eqvt: "p \<bullet> (atom a) = atom (p \<bullet> a)" |
1109 |
1114 |