equal
deleted
inserted
replaced
199 text {* There are known problems with syntax-declarations. They currently |
199 text {* There are known problems with syntax-declarations. They currently |
200 only work, when the context is already built. Hopefully this will be |
200 only work, when the context is already built. Hopefully this will be |
201 implemented correctly in future Isabelle versions. *} |
201 implemented correctly in future Isabelle versions. *} |
202 |
202 |
203 lemma |
203 lemma |
204 includes foo |
204 assumes "foo f a b c p1 i1 p2 i2 p3 i3 p4 i4" |
205 shows True |
205 shows True |
|
206 proof |
|
207 interpret foo [f a b c p1 i1 p2 i2 p3 i3 p4 i4] by fact |
206 term "s<a := i>\<cdot>a = i" |
208 term "s<a := i>\<cdot>a = i" |
207 by simp |
209 qed |
208 |
210 |
209 (* |
211 (* |
210 lemma |
212 lemma |
211 includes foo |
213 includes foo |
212 shows "s<a := i>\<cdot>a = i" |
214 shows "s<a := i>\<cdot>a = i" |