src/HOL/Imperative_HOL/Ref.thy
changeset 36176 3fe7e97ccca8
parent 34051 1a82e2e29d67
child 37709 70fafefbcc98
equal deleted inserted replaced
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: