Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/List.ML
Tue, 12 May 1998 08:36:07 +0200 nipkow Removed duplicate list_length_induct file | diff | annotate
Mon, 27 Apr 1998 16:45:11 +0200 nipkow Added a few lemmas. file | diff | annotate
Sat, 07 Mar 1998 16:29:29 +0100 nipkow Removed `addsplits [expand_if]' file | diff | annotate
Fri, 06 Mar 1998 15:19:29 +0100 nipkow expand_if is now by default part of the simpset. file | diff | annotate
Tue, 24 Feb 1998 10:44:53 +0100 nipkow Added some lemmas. file | diff | annotate
Sun, 22 Feb 1998 14:12:23 +0100 nipkow New induction schemas for lists (length and snoc). file | diff | annotate
Thu, 12 Feb 1998 17:53:05 +0100 wenzelm *** empty log message *** file | diff | annotate
Fri, 06 Feb 1998 18:55:18 +0100 nipkow Added `remdups' file | diff | annotate
Tue, 30 Dec 1997 11:14:09 +0100 nipkow nth -> ! file | diff | annotate
Tue, 16 Dec 1997 17:58:03 +0100 wenzelm expandshort; file | diff | annotate
Tue, 04 Nov 1997 20:47:38 +0100 oheimb added zip and nodup file | diff | annotate
Mon, 03 Nov 1997 12:13:18 +0100 wenzelm isatool fixclasimp; file | diff | annotate
Mon, 03 Nov 1997 08:08:14 +0100 nipkow expand_list_case -> split_list_case file | diff | annotate
Thu, 30 Oct 1997 09:45:03 +0100 nipkow For each datatype `t' there is now a theorem `split_t_case' of the form file | diff | annotate
Fri, 17 Oct 1997 15:25:12 +0200 nipkow setloop split_tac -> addsplits file | diff | annotate
Thu, 16 Oct 1997 15:09:08 +0200 nipkow Removed comment. file | diff | annotate
Thu, 16 Oct 1997 14:12:15 +0200 nipkow Various new lemmas. Improved conversion of equations to rewrite rules: file | diff | annotate
Tue, 14 Oct 1997 13:58:47 +0200 nipkow More lemmas, esp. ~Bex and ~Ball conversions. file | diff | annotate
Fri, 10 Oct 1997 19:02:28 +0200 wenzelm fixed dots; file | diff | annotate
Thu, 25 Sep 1997 12:13:18 +0200 paulson Changed some proofs to use Clarify_tac file | diff | annotate
Thu, 21 Aug 1997 12:53:23 +0200 paulson Renamed theorems of the form set_of_list_XXX to set_XXX file | diff | annotate
Tue, 05 Aug 1997 16:21:45 +0200 nipkow Added function `replicate' and lemmas map_cong and set_replicate. file | diff | annotate
Mon, 04 Aug 1997 11:50:35 +0200 nipkow Added a take/dropWhile lemma. file | diff | annotate
Fri, 01 Aug 1997 10:59:19 +0200 nipkow Generalized nth_drop (Conny). file | diff | annotate
Thu, 24 Jul 1997 15:25:29 +0200 nipkow Added a few lemmas. file | diff | annotate
Thu, 24 Jul 1997 11:12:18 +0200 nipkow List.ML: added lemmas by Stefan Merz. file | diff | annotate
Tue, 01 Jul 1997 10:34:30 +0200 paulson New laws for the "lists" operator file | diff | annotate
Mon, 30 Jun 1997 12:08:19 +0200 nipkow More concat lemmas. file | diff | annotate
Thu, 26 Jun 1997 13:20:50 +0200 nipkow set_of_list -> set file | diff | annotate
Mon, 23 Jun 1997 10:42:03 +0200 paulson Ran expandshort file | diff | annotate
Mon, 02 Jun 1997 12:13:42 +0200 paulson Corrected statement of filter_append; added filter_size file | diff | annotate
Mon, 26 May 1997 12:38:29 +0200 paulson New operator "lists" for formalizing sets of lists file | diff | annotate
Thu, 22 May 1997 13:05:52 +0200 nipkow Added rotation to exhaust_tac. file | diff | annotate
Thu, 22 May 1997 09:39:37 +0200 nipkow Replaced res_inst-list_cases by generic exhaust_tac. file | diff | annotate
Thu, 15 May 1997 12:54:02 +0200 paulson Added pred_list for TFL file | diff | annotate
Thu, 24 Apr 1997 18:06:46 +0200 nipkow Introduced a generic "induct_tac" which picks up the right induction scheme file | diff | annotate
Wed, 23 Apr 1997 09:14:56 +0200 nipkow Tidied up. file | diff | annotate
Fri, 04 Apr 1997 11:18:52 +0200 paulson Calls Blast_tac file | diff | annotate
Thu, 06 Mar 1997 16:05:32 +0100 pusch Minor changes due to primrec definition for nth file | diff | annotate
Wed, 12 Feb 1997 18:53:59 +0100 nipkow New class "order" and accompanying changes. file | diff | annotate
Fri, 17 Jan 1997 10:09:46 +0100 nipkow Got rid of Alls in List. file | diff | annotate
Thu, 12 Sep 1996 10:40:05 +0200 paulson Tidied many proofs, using AddIffs to let equivalences take file | diff | annotate
Thu, 22 Aug 1996 12:24:25 +0200 paulson Proved set_of_list_subset_Cons file | diff | annotate
Mon, 19 Aug 1996 11:12:38 +0200 paulson Renamed setOfList to set_of_list file | diff | annotate
Tue, 18 Jun 1996 16:20:30 +0200 paulson Addition of setOfList file | diff | annotate
Thu, 23 May 1996 14:37:06 +0200 berghofe Replaced fast_tac by Fast_tac (which uses default claset) file | diff | annotate
Wed, 06 Mar 1996 12:52:11 +0100 paulson Ran expandshort file | diff | annotate
Fri, 09 Feb 1996 13:41:18 +0100 nipkow Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec' file | diff | annotate
Tue, 30 Jan 1996 15:24:36 +0100 clasohm expanded tabs file | diff | annotate
Fri, 22 Dec 1995 12:25:20 +0100 nipkow defined take/drop by induction over list rather than nat. file | diff | annotate
Sun, 12 Nov 1995 16:29:12 +0100 nipkow added new arithmetic lemmas and the functions take and drop. file | diff | annotate
Wed, 25 Oct 1995 09:48:29 +0100 nipkow Added various thms and tactics. file | diff | annotate
Wed, 04 Oct 1995 13:10:03 +0100 clasohm added local simpsets; removed IOA from 'make test' file | diff | annotate
Thu, 27 Jul 1995 18:28:14 +0200 nipkow Added rev_append and rev_rev_ident to list_ss. file | diff | annotate
Thu, 29 Jun 1995 16:33:17 +0200 lcp Added function rev and its properties length_rev, etc. file | diff | annotate
Sun, 02 Apr 1995 10:43:59 +0200 nipkow generalized map (%x.x) xs = xs to map (%x.x) = (%xs.xs) file | diff | annotate
Mon, 27 Mar 1995 18:29:23 +0200 nipkow Added recursion equations for foldl to list_ss. file | diff | annotate
Fri, 17 Mar 1995 15:49:37 +0100 nipkow Added a few thms to nat_ss and list_ss file | diff | annotate
Fri, 03 Mar 1995 12:02:25 +0100 clasohm new version of HOL with curried function application file | diff | annotate
less more (0) tip
isabelle