changeset 37718 | 3046ebbb43c0 |
parent 37716 | 24bb91462892 |
child 37719 | 271ecd4fb9f9 |
--- a/src/HOL/Imperative_HOL/Relational.thy Mon Jul 05 15:25:42 2010 +0200 +++ b/src/HOL/Imperative_HOL/Relational.thy Mon Jul 05 15:36:37 2010 +0200 @@ -324,8 +324,6 @@ apply (elim crel_heap) unfolding Heap.ref_def apply (simp add: Let_def) - unfolding Heap.new_ref_def - apply (simp add: Let_def) unfolding ref_present_def apply auto unfolding get_ref_def set_ref_def