equal
deleted
inserted
replaced
181 locale E = fixes e defines e_def: "e(x) == x & x" |
181 locale E = fixes e defines e_def: "e(x) == x & x" |
182 notes e_def2 = e_def |
182 notes e_def2 = e_def |
183 |
183 |
184 lemma (in E) True thm e_def by fast |
184 lemma (in E) True thm e_def by fast |
185 |
185 |
186 interpretation p7: E ["(%x. x)"] by simp |
186 interpretation p7: E ["%x. x"] by simp |
187 |
187 |
188 (* TODO: goal mustn't be beta-reduced here, is doesn't match meta-hyp *) |
188 thm p7.e_def2 (* has no premise *) |
189 |
|
190 thm p7.e_def2 |
|
191 |
189 |
192 locale E' = fixes e defines e_def: "e == (%x. x & x)" |
190 locale E' = fixes e defines e_def: "e == (%x. x & x)" |
193 notes e_def2 = e_def |
191 notes e_def2 = e_def |
194 |
192 |
195 interpretation p7': E' ["(%x. x)"] by simp |
193 interpretation p7': E' ["(%x. x)"] by simp |