src/HOL/Imperative_HOL/Ref.thy
changeset 37845 b70d7a347964
parent 37842 27e7047d9ae6
child 37878 d016aaead7a2
--- a/src/HOL/Imperative_HOL/Ref.thy	Fri Jul 16 14:11:08 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy	Fri Jul 16 15:28:22 2010 +0200
@@ -303,3 +303,4 @@
 code_const Ref.update (Scala "('_: Unit)/ =>/ Heap.update((_), (_))")
 
 end
+