src/HOL/Imperative_HOL/Ref.thy
changeset 37878 d016aaead7a2
parent 37845 b70d7a347964
child 37965 0c1743d31b5c
equal deleted inserted replaced
37877:d4a30d210220 37878:d016aaead7a2
   294 code_const Ref.update (Haskell "Heap.writeSTRef")
   294 code_const Ref.update (Haskell "Heap.writeSTRef")
   295 
   295 
   296 
   296 
   297 text {* Scala *}
   297 text {* Scala *}
   298 
   298 
   299 code_type ref (Scala "!Heap.Ref[_]")
   299 code_type ref (Scala "!Ref[_]")
   300 code_const Ref (Scala "!error(\"bare Ref\")")
   300 code_const Ref (Scala "!error(\"bare Ref\")")
   301 code_const ref (Scala "('_: Unit)/ =>/ Heap.Ref((_))")
   301 code_const ref (Scala "('_: Unit)/ =>/ Ref((_))")
   302 code_const Ref.lookup (Scala "('_: Unit)/ =>/ Heap.lookup((_))")
   302 code_const Ref.lookup (Scala "('_: Unit)/ =>/ lookup((_))")
   303 code_const Ref.update (Scala "('_: Unit)/ =>/ Heap.update((_), (_))")
   303 code_const Ref.update (Scala "('_: Unit)/ =>/ update((_), (_))")
   304 
   304 
   305 end
   305 end
   306 
   306