src/HOL/List.thy
Sun, 31 Jan 2010 14:51:32 +0100 haftmann canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply
Thu, 21 Jan 2010 09:27:57 +0100 haftmann merged
Sat, 16 Jan 2010 17:15:28 +0100 haftmann dropped some old primrecs and some constdefs
Tue, 19 Jan 2010 17:53:11 +0100 hoelzl Added transpose_rectangle, when the input list is rectangular.
Tue, 19 Jan 2010 16:52:01 +0100 hoelzl Add transpose to the List-theory.
Fri, 15 Jan 2010 14:43:00 +0100 berghofe merged
Sun, 10 Jan 2010 18:09:11 +0100 berghofe same_append_eq / append_same_eq are now used for simplifying induction rules.
Wed, 13 Jan 2010 08:56:15 +0100 haftmann some syntax setup for Scala
Fri, 11 Dec 2009 14:43:55 +0100 haftmann avoid dependency on implicit dest rule predicate1D in proofs
Sat, 05 Dec 2009 20:02:21 +0100 haftmann tuned lattices theory fragements; generlized some lemmas from sets to lattices
Fri, 04 Dec 2009 12:22:09 +0100 haftmann merged
Mon, 30 Nov 2009 11:42:49 +0100 haftmann modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
Fri, 04 Dec 2009 08:26:25 +0100 nipkow added remdups_filter lemma
Thu, 12 Nov 2009 17:21:51 +0100 hoelzl Remove map_compose, replaced by map_map
Thu, 12 Nov 2009 17:21:48 +0100 hoelzl New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
Tue, 10 Nov 2009 16:11:37 +0100 haftmann tuned imports
Thu, 29 Oct 2009 11:41:36 +0100 haftmann moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Thu, 24 Sep 2009 18:29:29 +0200 haftmann lemma relating fold1 and foldl; code_unfold rules for Inf_fin, Sup_fin, Min, Max, Inf, Sup
Thu, 27 Aug 2009 11:41:07 +0200 nipkow code generator: quantifiers over {_.._::int} and {_..<_::nat}
Thu, 27 Aug 2009 09:28:52 +0200 nipkow tuned code generation for lists
Wed, 26 Aug 2009 19:54:01 +0200 nipkow got rid of complicated class finite_intvl_succ and defined "upto" directly on int, the only instance of the class.
Mon, 20 Jul 2009 09:52:09 +0200 haftmann merged
Wed, 15 Jul 2009 16:00:06 +0200 haftmann merged
Mon, 20 Jul 2009 08:32:07 +0200 haftmann merged
Tue, 14 Jul 2009 16:27:32 +0200 haftmann prefer code_inline over code_unfold; use code_unfold_post where appropriate
Wed, 15 Jul 2009 23:48:21 +0200 wenzelm more antiquotations;
Wed, 15 Jul 2009 20:34:58 +0200 nipkow Made "prime" executable
Wed, 15 Jul 2009 12:44:41 +0200 nipkow made upt/upto executable on nat/int by simp
Tue, 14 Jul 2009 10:54:04 +0200 haftmann code attributes use common underscore convention
Fri, 03 Jul 2009 08:44:13 +0200 haftmann lemma foldl_apply_inv
Tue, 23 Jun 2009 16:27:12 +0200 haftmann tuned interfaces of datatype module
Fri, 19 Jun 2009 17:23:21 +0200 haftmann discontinued ancient tradition to suffix certain ML module names with "_package"
Thu, 11 Jun 2009 23:24:28 +0200 nipkow two finiteness lemmas by Robert Himmelmann
Thu, 04 Jun 2009 15:28:59 +0200 haftmann lemma about List.foldl and Finite_Set.fold
Tue, 02 Jun 2009 13:59:32 +0200 hoelzl Added theorems about distinct & concat, map & replicate and concat & replicate
Wed, 27 May 2009 07:56:11 +0200 nipkow more lemmas
Tue, 26 May 2009 10:31:39 -0700 huffman listsum lemmas
Tue, 19 May 2009 13:52:12 +0200 nipkow new lemma
Fri, 15 May 2009 10:01:57 +0200 nipkow new lemma
Thu, 14 May 2009 15:09:47 +0200 haftmann preprocessing must consider eq
Sat, 09 May 2009 07:25:22 +0200 nipkow lemmas by Andreas Lochbihler
Fri, 08 May 2009 08:06:43 +0200 nipkow more lemmas
Wed, 06 May 2009 19:09:31 +0200 haftmann proper structures for list and string code generation stuff
Wed, 06 May 2009 16:01:06 +0200 haftmann refined HOL string theories and corresponding ML fragments
Wed, 29 Apr 2009 21:10:46 +0200 nipkow added listsum lemmas
Fri, 24 Apr 2009 17:45:15 +0200 haftmann funpow and relpow with shared "^^" syntax
Mon, 20 Apr 2009 09:32:07 +0200 haftmann power operation on functions with syntax o^; power operation on relations with syntax ^^
Fri, 17 Apr 2009 15:57:26 +0200 haftmann separated funpow, relpow from power on monoids
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Mon, 02 Mar 2009 16:53:55 +0100 nipkow name changes
Thu, 26 Feb 2009 08:44:12 -0800 huffman revert some Suc 0 lemmas back to their original forms; added some simp rules for (1::nat)
Mon, 23 Feb 2009 16:25:52 -0800 huffman make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
Fri, 20 Feb 2009 10:14:32 +0100 haftmann defensive implementation of pretty serialisation of lists and characters
Mon, 16 Feb 2009 10:13:30 +0100 blanchet Added nitpick attribute, and fixed typo.
Tue, 10 Feb 2009 17:53:51 -0800 huffman const_name antiquotations
Sat, 07 Feb 2009 09:57:07 +0100 haftmann code theorems for nth, list_update
Sat, 07 Feb 2009 08:37:43 +0100 haftmann code theorems for nth, list_update
Fri, 06 Feb 2009 15:15:27 +0100 haftmann authentic syntax for List.nth
less more (0) -300 -100 -60 tip