Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Imperative_HOL/Relational.thy
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
isabelle