equal
deleted
inserted
replaced
172 |
172 |
173 inductive |
173 inductive |
174 tt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" |
174 tt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" |
175 for r :: "('a \<Rightarrow> 'a \<Rightarrow> bool)" |
175 for r :: "('a \<Rightarrow> 'a \<Rightarrow> bool)" |
176 where |
176 where |
177 "tt r a b" |
177 aa: "tt r a a" |
178 | "tt r a b ==> tt r a c" |
178 | bb: "tt r a b ==> tt r a c" |
179 |
179 |
180 (* |
180 (* PROBLEM: derived eqvt-theorem does not conform with [eqvt] |
181 equivariance tt |
181 equivariance tt |
182 *) |
182 *) |
183 |
183 |
184 |
184 |
185 inductive |
185 inductive |