src/HOL/List.thy
changeset 22793 dc13dfd588b2
parent 22633 a47e4fd7ebc1
child 22799 ed7d53db2170
equal deleted inserted replaced
22792:2443ae6dac7d 22793:dc13dfd588b2
  2198  "splice (x#xs) (y#ys) = x # y # splice xs ys"
  2198  "splice (x#xs) (y#ys) = x # y # splice xs ys"
  2199 by simp
  2199 by simp
  2200 
  2200 
  2201 declare splice.simps(2) [simp del, code del]
  2201 declare splice.simps(2) [simp del, code del]
  2202 
  2202 
       
  2203 lemma length_splice[simp]: "!!ys. length(splice xs ys) = length xs + length ys"
       
  2204 apply(induct xs) apply simp
       
  2205 apply(case_tac ys)
       
  2206  apply auto
       
  2207 done
       
  2208 
  2203 subsubsection{*Sets of Lists*}
  2209 subsubsection{*Sets of Lists*}
  2204 
  2210 
  2205 subsubsection {* @{text lists}: the list-forming operator over sets *}
  2211 subsubsection {* @{text lists}: the list-forming operator over sets *}
  2206 
  2212 
  2207 inductive2
  2213 inductive2