src/HOL/Imperative_HOL/Ref.thy
changeset 38771 f9cd27cbe8a4
parent 38068 00042fd999a8
child 38968 e55deaa22fff
equal deleted inserted replaced
38770:1c70a502c590 38771:f9cd27cbe8a4
   304 code_const Ref.update (Haskell "Heap.writeSTRef")
   304 code_const Ref.update (Haskell "Heap.writeSTRef")
   305 
   305 
   306 
   306 
   307 text {* Scala *}
   307 text {* Scala *}
   308 
   308 
   309 code_type ref (Scala "!Ref[_]")
   309 code_type ref (Scala "!Heap.Ref[_]")
   310 code_const Ref (Scala "!error(\"bare Ref\")")
   310 code_const Ref (Scala "!error(\"bare Ref\")")
   311 code_const ref' (Scala "('_: Unit)/ =>/ Ref((_))")
   311 code_const ref' (Scala "('_: Unit)/ =>/ Heap.Ref((_))")
   312 code_const Ref.lookup (Scala "('_: Unit)/ =>/ Ref.lookup((_))")
   312 code_const Ref.lookup (Scala "('_: Unit)/ =>/ Heap.Ref.lookup((_))")
   313 code_const Ref.update (Scala "('_: Unit)/ =>/ Ref.update((_), (_))")
   313 code_const Ref.update (Scala "('_: Unit)/ =>/ Heap.Ref.update((_), (_))")
   314 
   314 
   315 end
   315 end