src/HOL/List.ML
1998-04-27 nipkow 1998-04-27 Added a few lemmas. Renamed expand_const -> split_const.
1998-03-07 nipkow 1998-03-07 Removed `addsplits [expand_if]'
1998-03-06 nipkow 1998-03-06 expand_if is now by default part of the simpset.
1998-02-24 nipkow 1998-02-24 Added some lemmas.
1998-02-22 nipkow 1998-02-22 New induction schemas for lists (length and snoc).
1998-02-12 wenzelm 1998-02-12 *** empty log message ***
1998-02-06 nipkow 1998-02-06 Added `remdups' nodup -> nodups
1997-12-30 nipkow 1997-12-30 nth -> !
1997-12-16 wenzelm 1997-12-16 expandshort;
1997-11-04 oheimb 1997-11-04 added zip and nodup
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-11-03 nipkow 1997-11-03 expand_list_case -> split_list_case
1997-10-30 nipkow 1997-10-30 For each datatype `t' there is now a theorem `split_t_case' of the form P(t_case f1 ... fn x) = ((!y1 ... ym1. x = C1 y1 ... ym1 --> P(f1 y1 ... ym1))& ... (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))) The simplifier now reduces !x. (..x.. & x = t & ..x..) --> P x to (..t.. & ..t..) --> P t (and similarly for t=x).
1997-10-17 nipkow 1997-10-17 setloop split_tac -> addsplits
1997-10-16 nipkow 1997-10-16 Removed comment.
1997-10-16 nipkow 1997-10-16 Various new lemmas. Improved conversion of equations to rewrite rules: (s=t becomes (s=t)==True if s=t loops).
1997-10-14 nipkow 1997-10-14 More lemmas, esp. ~Bex and ~Ball conversions.
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-09-25 paulson 1997-09-25 Changed some proofs to use Clarify_tac
1997-08-21 paulson 1997-08-21 Renamed theorems of the form set_of_list_XXX to set_XXX
1997-08-05 nipkow 1997-08-05 Added function `replicate' and lemmas map_cong and set_replicate.
1997-08-04 nipkow 1997-08-04 Added a take/dropWhile lemma.
1997-08-01 nipkow 1997-08-01 Generalized nth_drop (Conny).
1997-07-24 nipkow 1997-07-24 Added a few lemmas.
1997-07-24 nipkow 1997-07-24 List.ML: added lemmas by Stefan Merz. simpodata.ML: removed rules about ? now subsumed by simplification proc.
1997-07-01 paulson 1997-07-01 New laws for the "lists" operator
1997-06-30 nipkow 1997-06-30 More concat lemmas.
1997-06-26 nipkow 1997-06-26 set_of_list -> set
1997-06-23 paulson 1997-06-23 Ran expandshort
1997-06-02 paulson 1997-06-02 Corrected statement of filter_append; added filter_size
1997-05-26 paulson 1997-05-26 New operator "lists" for formalizing sets of lists
1997-05-22 nipkow 1997-05-22 Added rotation to exhaust_tac.
1997-05-22 nipkow 1997-05-22 Replaced res_inst-list_cases by generic exhaust_tac.
1997-05-15 paulson 1997-05-15 Added pred_list for TFL
1997-04-24 nipkow 1997-04-24 Introduced a generic "induct_tac" which picks up the right induction scheme automatically. Also changed nat_ind_tac, which does no longer append a "1" to the name of the induction variable. This caused some changes...
1997-04-23 nipkow 1997-04-23 Tidied up.
1997-04-04 paulson 1997-04-04 Calls Blast_tac
1997-03-06 pusch 1997-03-06 Minor changes due to primrec definition for nth
1997-02-12 nipkow 1997-02-12 New class "order" and accompanying changes. In particular reflexivity of <= is now one rewrite rule.
1997-01-17 nipkow 1997-01-17 Got rid of Alls in List. Added Ball_insert and Ball_Un in equalities.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