src/HOL/Library/More_List.thy
changeset 58881 b9556a055632
parent 58437 8d124c73c37a
child 60500 903bb1495239
equal deleted inserted replaced
58880:0baae4311a9f 58881:b9556a055632
     1 (* Author: Andreas Lochbihler, ETH Zürich
     1 (* Author: Andreas Lochbihler, ETH Zürich
     2    Author: Florian Haftmann, TU Muenchen  *)
     2    Author: Florian Haftmann, TU Muenchen  *)
     3 
     3 
     4 header \<open>Less common functions on lists\<close>
     4 section \<open>Less common functions on lists\<close>
     5 
     5 
     6 theory More_List
     6 theory More_List
     7 imports Main
     7 imports Main
     8 begin
     8 begin
     9 
     9