equal
deleted
inserted
replaced
157 thm FV_kind_def |
157 thm FV_kind_def |
158 thm FV_ty_def |
158 thm FV_ty_def |
159 thm FV_trm_def |
159 thm FV_trm_def |
160 |
160 |
161 (* FIXME: does not work yet *) |
161 (* FIXME: does not work yet *) |
162 (* |
|
163 overloading |
162 overloading |
164 perm_kind \<equiv> "perm :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND" (unchecked) |
163 perm_kind \<equiv> "perm :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND" (unchecked) |
165 perm_ty \<equiv> "perm :: 'x prm \<Rightarrow> TY \<Rightarrow> TY" (unchecked) |
164 perm_ty \<equiv> "perm :: 'x prm \<Rightarrow> TY \<Rightarrow> TY" (unchecked) |
166 perm_trm \<equiv> "perm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM" (unchecked) |
165 perm_trm \<equiv> "perm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM" (unchecked) |
167 begin |
166 begin |
168 |
167 |
169 quotient_def |
168 quotient_def |
170 perm_kind :: "'x prm \<Rightarrow> KIND \<Rightarrow> KIND" |
169 perm_kind :: "'x prm \<Rightarrow> KIND \<Rightarrow> KIND" |
171 where |
170 where |
172 "perm_kind \<equiv> (perm::'x prm \<Rightarrow> KIND \<Rightarrow> KIND)" |
171 "perm_kind \<equiv> (perm::'x prm \<Rightarrow> kind \<Rightarrow> kind)" |
|
172 |
|
173 quotient_def |
|
174 perm_ty :: "'x prm \<Rightarrow> TY \<Rightarrow> TY" |
|
175 where |
|
176 "perm_ty \<equiv> (perm::'x prm \<Rightarrow> ty \<Rightarrow> ty)" |
|
177 |
|
178 quotient_def |
|
179 perm_trm :: "'x prm \<Rightarrow> TRM \<Rightarrow> TRM" |
|
180 where |
|
181 "perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)" |
|
182 |
173 end |
183 end |
174 *) |
|
175 |
184 |
|
185 |
|
186 |