src/HOL/List.thy
Fri, 19 Oct 2012 15:12:52 +0200 webertj Renamed {left,right}_distrib to distrib_{right,left}.
Sat, 20 Oct 2012 09:12:16 +0200 haftmann moved quite generic material from theory Enum to more appropriate places
Wed, 10 Oct 2012 15:16:44 +0200 Andreas Lochbihler tail-recursive implementation for length
Tue, 09 Oct 2012 16:57:58 +0200 kuncar rename Set.project to Set.filter - more appropriate name
Mon, 08 Oct 2012 12:03:49 +0200 haftmann consolidated names of theorems on composition;
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Thu, 16 Aug 2012 14:07:32 +0200 haftmann prefer eta-expanded code equations for fold, to accomodate tail recursion optimisation in Scala
Tue, 31 Jul 2012 13:55:39 +0200 kuncar more set operations expressed by Finite_Set.fold
Mon, 30 Apr 2012 12:14:53 +0200 bulwahn making sorted_list_of_set executable
Sat, 21 Apr 2012 06:49:04 +0200 huffman strengthen rule list_all2_induct
Thu, 12 Apr 2012 11:01:15 +0200 bulwahn merged
Tue, 03 Apr 2012 17:26:30 +0900 griff renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
Fri, 06 Apr 2012 19:23:51 +0200 haftmann abandoned almost redundant *_foldr lemmas
Fri, 06 Apr 2012 19:18:00 +0200 haftmann tuned
Fri, 06 Apr 2012 18:17:16 +0200 haftmann no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
Mon, 26 Mar 2012 21:00:23 +0200 nipkow reverted to canonical name
Mon, 26 Mar 2012 18:54:41 +0200 nipkow Functions and lemmas by Christian Sternagel
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Tue, 13 Mar 2012 13:31:26 +0100 wenzelm tuned proofs -- eliminated pointless chaining of facts after 'interpret';
Mon, 12 Mar 2012 21:41:11 +0100 noschinl tuned proofs
Mon, 27 Feb 2012 09:01:49 +0100 nipkow converting "set [...]" to "{...}" in evaluation results
Sat, 25 Feb 2012 09:07:37 +0100 bulwahn one general list_all2_update_cong instead of two special ones
Fri, 24 Feb 2012 22:46:44 +0100 haftmann moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
Fri, 24 Feb 2012 09:40:02 +0100 haftmann given up disfruitful branch
Thu, 23 Feb 2012 21:25:59 +0100 haftmann moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
Thu, 16 Feb 2012 09:18:23 +0100 bulwahn removing unnecessary premises in theorems of List theory
Fri, 10 Feb 2012 09:47:59 +0100 Cezary Kaliszyk more specification of the quotient package in IsarRef
Wed, 08 Feb 2012 01:49:33 +0100 blanchet use 'primrec' to define "rotate1", for uniformity (and to help first-order tools that rely on "Spec_Rules")
Wed, 08 Feb 2012 00:55:06 +0100 blanchet removed fact that confuses SPASS -- better rely on "rev_rev_ident", which is stronger and more ATP friendly
Sun, 05 Feb 2012 10:43:52 +0100 bulwahn adding code equation for Relation.image; adding map_project as correspondence to map_filter on lists
Sun, 05 Feb 2012 08:24:39 +0100 bulwahn another try to improve code generation of set equality (cf. da32cf32c0c7)
Thu, 02 Feb 2012 10:12:30 +0100 bulwahn adding a minimally refined equality on sets for code generation
Tue, 31 Jan 2012 15:39:45 +0100 bulwahn adding code equation for setsum
Mon, 23 Jan 2012 17:29:19 +0100 huffman generalize type of List.listrel
Mon, 23 Jan 2012 14:07:36 +0100 bulwahn adding code generation for some list relations
Tue, 10 Jan 2012 18:12:03 +0100 berghofe pred_subset/equals_eq are now standard pred_set_conv rules
Sat, 07 Jan 2012 20:44:23 +0100 haftmann massaging of code setup for sets
Sat, 07 Jan 2012 11:45:53 +0100 haftmann corrected slip
Sat, 07 Jan 2012 09:32:01 +0100 haftmann restore convenient code_abbrev declarations (particulary important if List.set is not the formal constructor for sets)
Fri, 06 Jan 2012 22:16:01 +0100 haftmann moved lemmas about List.set and set operations to List theory
Fri, 06 Jan 2012 20:39:50 +0100 haftmann farewell to theory More_List
Fri, 06 Jan 2012 17:44:42 +0100 wenzelm improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
Fri, 06 Jan 2012 10:19:49 +0100 haftmann incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
Thu, 05 Jan 2012 18:18:39 +0100 wenzelm improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
Thu, 29 Dec 2011 13:42:21 +0100 haftmann qualified Finite_Set.fold
Thu, 29 Dec 2011 10:47:55 +0100 haftmann attribute code_abbrev superseedes code_unfold_post; tuned text
Tue, 27 Dec 2011 09:15:26 +0100 haftmann dropped fact whose names clash with corresponding facts on canonical fold
Sat, 24 Dec 2011 15:53:10 +0100 haftmann dropped obsolete lemma member_set
Mon, 19 Dec 2011 14:41:08 +0100 noschinl add lemmas
Thu, 15 Dec 2011 18:08:40 +0100 wenzelm clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
Tue, 13 Dec 2011 22:44:16 +0100 noschinl added lemmas
Fri, 09 Dec 2011 13:42:16 +0100 huffman add induction rule for list_all2
Thu, 08 Dec 2011 13:53:27 +0100 bulwahn removing special code generator setup for hd and last function because this causes problems with quickcheck narrowing as the Haskell Prelude functions throw errors that cannot be caught instead of PatternFail exceptions
Thu, 01 Dec 2011 15:41:58 +0100 hoelzl cardinality of sets of lists
Sun, 20 Nov 2011 21:07:10 +0100 wenzelm eliminated obsolete "standard";
Wed, 19 Oct 2011 08:37:27 +0200 bulwahn removing old code generator setup for lists
Mon, 03 Oct 2011 14:43:12 +0200 bulwahn adding lemma to List library for executable equation of the (refl) transitive closure
Wed, 14 Sep 2011 10:08:52 -0400 hoelzl renamed Complete_Lattices lemmas, removed legacy names
Tue, 13 Sep 2011 17:07:33 -0700 huffman tuned proofs
Tue, 13 Sep 2011 12:14:29 +0200 bulwahn added lemma motivated by a more specific lemma in the AFP-KBPs theories
less more (0) -300 -100 -60 tip