equal
deleted
inserted
replaced
16 |
16 |
17 record point2d = |
17 record point2d = |
18 xc :: int |
18 xc :: int |
19 yc :: int |
19 yc :: int |
20 |
20 |
21 (* FIXME: Invalid intermediate term |
|
22 lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x, yc := y\<rparr>" |
21 lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x, yc := y\<rparr>" |
23 nitpick [expect = none] |
22 nitpick [expect = none] |
24 sorry |
23 sorry |
25 |
24 |
26 lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x\<rparr>" |
25 lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x\<rparr>" |
82 oops |
81 oops |
83 |
82 |
84 lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> = p" |
83 lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> = p" |
85 nitpick [expect = genuine] |
84 nitpick [expect = genuine] |
86 oops |
85 oops |
87 *) |
|
88 |
86 |
89 end |
87 end |