src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
changeset 47108 2a1953f0d20d
parent 44890 22f665a2e91c
child 50630 1ea90e8046dc
     1.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* An imperative in-place reversal on arrays *}
     1.5  
     1.6  theory Imperative_Reverse
     1.7 -imports Subarray Imperative_HOL
     1.8 +imports Subarray "~~/src/HOL/Imperative_HOL/Imperative_HOL"
     1.9  begin
    1.10  
    1.11  fun swap :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
    1.12 @@ -107,7 +107,7 @@
    1.13    shows "Array.get h' a = List.rev (Array.get h a)"
    1.14    using rev2_rev'[OF assms] rev_length[OF assms] assms
    1.15      by (cases "Array.length h a = 0", auto simp add: Array.length_def
    1.16 -      subarray_def sublist'_all rev.simps[where j=0] elim!: effect_elims)
    1.17 +      subarray_def rev.simps[where j=0] elim!: effect_elims)
    1.18    (drule sym[of "List.length (Array.get h a)"], simp)
    1.19  
    1.20  definition "example = (Array.make 10 id \<guillemotright>= (\<lambda>a. rev a 0 9))"
    1.21 @@ -115,3 +115,4 @@
    1.22  export_code example checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp?
    1.23  
    1.24  end
    1.25 +