equal
deleted
inserted
replaced
207 print_interps! IA |
207 print_interps! IA |
208 fix beta and gamma |
208 fix beta and gamma |
209 interpret i9: ID [a beta _] |
209 interpret i9: ID [a beta _] |
210 apply - apply assumption |
210 apply - apply assumption |
211 apply unfold_locales |
211 apply unfold_locales |
|
212 apply (rule refl) (*FIXME: should have been discharged by unfold_locales*) |
212 apply (rule refl) done |
213 apply (rule refl) done |
213 qed rule |
214 qed rule |
214 |
215 |
215 |
216 |
216 (* Definition involving free variable *) |
217 (* Definition involving free variable *) |