equal
deleted
inserted
replaced
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? Scala? |
113 export_code rev checking SML SML_imp OCaml? OCaml_imp? Haskell? (*Scala?*) |
114 |
114 |
115 end |
115 end |