src/HOL/List.ML
1996-09-12 paulson 1996-09-12 Tidied many proofs, using AddIffs to let equivalences take the place of separate Intr and Elim rules. Also deleted most named clasets.
1996-08-22 paulson 1996-08-22 Proved set_of_list_subset_Cons
1996-08-19 paulson 1996-08-19 Renamed setOfList to set_of_list
1996-06-18 paulson 1996-06-18 Addition of setOfList
1996-05-23 berghofe 1996-05-23 Replaced fast_tac by Fast_tac (which uses default claset) New rules are now also added to default claset.
1996-03-06 paulson 1996-03-06 Ran expandshort
1996-02-09 nipkow 1996-02-09 Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-12-22 nipkow 1995-12-22 defined take/drop by induction over list rather than nat.
1995-11-12 nipkow 1995-11-12 added new arithmetic lemmas and the functions take and drop.
1995-10-25 nipkow 1995-10-25 Added various thms and tactics.
1995-10-04 clasohm 1995-10-04 added local simpsets; removed IOA from 'make test'
1995-07-27 nipkow 1995-07-27 Added rev_append and rev_rev_ident to list_ss.
1995-06-29 lcp 1995-06-29 Added function rev and its properties length_rev, etc.
1995-04-02 nipkow 1995-04-02 generalized map (%x.x) xs = xs to map (%x.x) = (%xs.xs)
1995-03-27 nipkow 1995-03-27 Added recursion equations for foldl to list_ss.
1995-03-17 nipkow 1995-03-17 Added a few thms to nat_ss and list_ss
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application