src/HOL/Imperative_HOL/Array.thy
changeset 38771 f9cd27cbe8a4
parent 37964 0a1ae22df1f1
child 38968 e55deaa22fff
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Wed Aug 25 22:47:04 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Thu Aug 26 10:16:22 2010 +0200
     1.3 @@ -484,11 +484,11 @@
     1.4  
     1.5  code_type array (Scala "!collection.mutable.ArraySeq[_]")
     1.6  code_const Array (Scala "!error(\"bare Array\")")
     1.7 -code_const Array.new' (Scala "('_: Unit)/ => / Array.alloc((_))((_))")
     1.8 -code_const Array.make' (Scala "('_: Unit)/ =>/ Array.make((_))((_))")
     1.9 -code_const Array.len' (Scala "('_: Unit)/ =>/ Array.len((_))")
    1.10 -code_const Array.nth' (Scala "('_: Unit)/ =>/ Array.nth((_), (_))")
    1.11 -code_const Array.upd' (Scala "('_: Unit)/ =>/ Array.upd((_), (_), (_))")
    1.12 -code_const Array.freeze (Scala "('_: Unit)/ =>/ Array.freeze((_))")
    1.13 +code_const Array.new' (Scala "('_: Unit)/ => / Heap.Array.alloc((_))((_))")
    1.14 +code_const Array.make' (Scala "('_: Unit)/ =>/ Heap.Array.make((_))((_))")
    1.15 +code_const Array.len' (Scala "('_: Unit)/ =>/ Heap.Array.len((_))")
    1.16 +code_const Array.nth' (Scala "('_: Unit)/ =>/ Heap.Array.nth((_), (_))")
    1.17 +code_const Array.upd' (Scala "('_: Unit)/ =>/ Heap.Array.upd((_), (_), (_))")
    1.18 +code_const Array.freeze (Scala "('_: Unit)/ =>/ Heap.Array.freeze((_))")
    1.19  
    1.20  end