src/HOL/Imperative_HOL/Array.thy
changeset 38968 e55deaa22fff
parent 38771 f9cd27cbe8a4
child 39198 f967a16dfcdd
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Wed Sep 01 09:03:34 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Wed Sep 01 11:09:50 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)/ => / Heap.Array.alloc((_))((_))")
     1.8 -code_const Array.make' (Scala "('_: Unit)/ =>/ Heap.Array.make((_))((_))")
     1.9 -code_const Array.len' (Scala "('_: Unit)/ =>/ Heap.Array.len((_))")
    1.10 -code_const Array.nth' (Scala "('_: Unit)/ =>/ Heap.Array.nth((_), (_))")
    1.11 -code_const Array.upd' (Scala "('_: Unit)/ =>/ Heap.Array.upd((_), (_), (_))")
    1.12 -code_const Array.freeze (Scala "('_: Unit)/ =>/ Heap.Array.freeze((_))")
    1.13 +code_const Array.new' (Scala "('_: Unit)/ => / Array.alloc((_))((_))")
    1.14 +code_const Array.make' (Scala "('_: Unit)/ =>/ Array.make((_))((_))")
    1.15 +code_const Array.len' (Scala "('_: Unit)/ =>/ Array.len((_))")
    1.16 +code_const Array.nth' (Scala "('_: Unit)/ =>/ Array.nth((_), (_))")
    1.17 +code_const Array.upd' (Scala "('_: Unit)/ =>/ Array.upd((_), (_), (_))")
    1.18 +code_const Array.freeze (Scala "('_: Unit)/ =>/ Array.freeze((_))")
    1.19  
    1.20  end