src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
changeset 37826 4c0a5e35931a
parent 37806 a7679be14442
child 37845 b70d7a347964
equal deleted inserted replaced
37825:adc1143bc1a8 37826:4c0a5e35931a
   108   using rev2_rev'[OF assms] rev_length[OF assms] assms
   108   using rev2_rev'[OF assms] rev_length[OF assms] assms
   109     by (cases "Array.length h a = 0", auto simp add: Array.length_def
   109     by (cases "Array.length h a = 0", auto simp add: Array.length_def
   110       subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims)
   110       subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims)
   111   (drule sym[of "List.length (Array.get h a)"], simp)
   111   (drule sym[of "List.length (Array.get h a)"], simp)
   112 
   112 
       
   113 export_code rev checking SML SML_imp OCaml? OCaml_imp? Haskell?
       
   114 
   113 end
   115 end