changeset 36176 | 3fe7e97ccca8 |
parent 34051 | 1a82e2e29d67 |
child 37709 | 70fafefbcc98 |
36175:5cec4ca719d1 | 36176:3fe7e97ccca8 |
---|---|
39 let y = f x; |
39 let y = f x; |
40 r := y; |
40 r := y; |
41 return y |
41 return y |
42 done)" |
42 done)" |
43 |
43 |
44 hide (open) const new lookup update change |
44 hide_const (open) new lookup update change |
45 |
45 |
46 |
46 |
47 subsection {* Properties *} |
47 subsection {* Properties *} |
48 |
48 |
49 lemma lookup_chain: |
49 lemma lookup_chain: |