src/HOL/List.thy
Thu, 17 Aug 2017 07:27:17 +0200 nipkow added lemma
Wed, 16 Aug 2017 21:14:11 +0200 nipkow more reorganization around sorted_wrt
Tue, 15 Aug 2017 19:47:08 +0200 nipkow added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
Sun, 06 Aug 2017 21:49:25 +0200 bulwahn slightly generalized card_lists_distinct_length_eq; renamed specialized card_lists_distinct_length_eq to card_lists_distinct_length_eq'; tuned
Sat, 08 Jul 2017 17:33:11 +0200 nipkow revised lemma
Sat, 08 Jul 2017 15:51:29 +0200 nipkow generalized lemma
Fri, 07 Jul 2017 11:32:06 +0200 nipkow added lemma
Mon, 29 May 2017 09:14:15 +0200 eberlm reorganised material on sublists
Mon, 03 Apr 2017 16:56:45 +0200 eberlm added shuffle product to HOL/List
Sun, 29 Jan 2017 17:27:02 +0100 wenzelm added inj_def (redundant, analogous to surj_def, bij_def);
Sun, 29 Jan 2017 13:28:45 +0100 wenzelm tuned whitespace;
Thu, 12 Jan 2017 15:54:13 +0100 blanchet added lemma
Mon, 17 Oct 2016 17:33:07 +0200 nipkow setprod -> prod
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Fri, 16 Sep 2016 21:28:09 +0200 wenzelm more symbols;
Sun, 11 Sep 2016 00:14:44 +0200 wenzelm tuned proofs;
Wed, 24 Aug 2016 11:02:23 +0200 nipkow added lemma
Wed, 10 Aug 2016 18:57:20 +0200 haftmann lists form a monoid
Fri, 29 Jul 2016 09:49:23 +0200 Andreas Lochbihler add lemmas contributed by Peter Gammie
Fri, 22 Jul 2016 11:00:43 +0200 wenzelm tuned proofs -- avoid unstructured calculation;
Tue, 19 Jul 2016 14:09:55 +0200 Lars Hupel added missing transfer rule
Sat, 02 Jul 2016 08:41:05 +0200 haftmann more theorems
Wed, 22 Jun 2016 10:09:20 +0200 wenzelm bundle lifting_syntax;
Thu, 16 Jun 2016 17:57:09 +0200 eberlm Various additions to polynomials, FPSs, Gamma function
Sun, 29 May 2016 14:10:48 +0200 nipkow added subtheory of longest common prefix
Wed, 25 May 2016 11:49:40 +0200 wenzelm isabelle update_cartouches -c -t;
Tue, 17 May 2016 17:05:35 +0200 eberlm Moved material from AFP/Randomised_Social_Choice to distribution
Fri, 13 May 2016 20:24:10 +0200 wenzelm eliminated use of empty "assms";
Mon, 25 Apr 2016 16:09:26 +0200 wenzelm eliminated old 'def';
Thu, 10 Mar 2016 12:33:01 +0100 haftmann moved
Tue, 23 Feb 2016 16:25:08 +0100 nipkow more canonical names
Wed, 17 Feb 2016 21:51:56 +0100 haftmann prefer abbreviations for compound operators INFIMUM and SUPREMUM
Wed, 17 Feb 2016 11:39:26 +0100 traytel call the predicator of list list_all
Wed, 13 Jan 2016 23:07:06 +0100 wenzelm isabelle update_cartouches -c -t;
Fri, 08 Jan 2016 16:37:56 +0100 wenzelm merged
Thu, 07 Jan 2016 15:53:39 +0100 wenzelm more uniform treatment of package internals;
Fri, 08 Jan 2016 16:36:41 +0100 nipkow added lemma
Tue, 05 Jan 2016 17:54:10 +0100 eberlm Added some facts about polynomials
Mon, 28 Dec 2015 21:47:32 +0100 wenzelm former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
Sun, 27 Dec 2015 17:16:21 +0100 wenzelm discontinued ASCII replacement syntax <->;
Thu, 10 Dec 2015 13:38:40 +0000 paulson not_leE -> not_le_imp_less and other tidying
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Wed, 18 Nov 2015 15:23:34 +0000 paulson New theorems mostly from Peter Gammie
Sun, 15 Nov 2015 13:49:27 +0100 wenzelm merged
Sun, 15 Nov 2015 12:39:51 +0100 wenzelm option "inductive_defs" controls exposure of def and mono facts;
Sat, 14 Nov 2015 08:45:51 +0100 haftmann reverted half-baken 7d1127ac2251
Wed, 11 Nov 2015 09:48:24 +0100 Andreas Lochbihler add various lemmas
Mon, 09 Nov 2015 15:48:17 +0100 wenzelm qualifier is mandatory by default;
Wed, 04 Nov 2015 08:13:52 +0100 ballarin Keyword 'rewrites' identifies rewrite morphisms.
Sat, 17 Oct 2015 16:08:30 +0200 haftmann code abbreviation for mapping over a fixed range
Fri, 09 Oct 2015 20:26:03 +0200 wenzelm discontinued specific HTML syntax;
Sun, 13 Sep 2015 22:56:52 +0200 wenzelm tuned proofs -- less legacy;
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>;
Thu, 27 Aug 2015 21:19:48 +0200 haftmann standardized some occurences of ancient "split" alias
Thu, 27 Aug 2015 13:07:45 +0200 haftmann more lemmas on sorting and multisets (due to Thomas Sewell)
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Sat, 18 Jul 2015 20:47:08 +0200 wenzelm prefer tactics with explicit context;
Thu, 25 Jun 2015 23:33:47 +0200 wenzelm tuned proofs;
Mon, 22 Jun 2015 11:15:23 +0200 nipkow modernized name
Thu, 30 Apr 2015 16:07:43 +0200 wenzelm more formal source, more PIDE markup;
less more (0) -300 -100 -60 tip