src/HOL/List.thy
Sat, 25 May 2013 15:44:29 +0200 haftmann weaker precendence of syntax for big intersection and union on sets
Fri, 24 May 2013 17:00:46 +0200 wenzelm tuned signature;
Thu, 23 May 2013 14:22:49 +0200 noschinl more lemmas for sorted_list_of_set
Mon, 06 May 2013 02:48:18 +0200 nipkow tail recursive version of map, for code generation, optionally
Tue, 23 Apr 2013 11:14:51 +0200 haftmann tuned: unnamed contexts, interpretation and sublocale in locale target;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Fri, 05 Apr 2013 22:08:42 +0200 traytel allow redundant cases in the list comprehension translation
Tue, 22 Jan 2013 14:33:45 +0100 traytel separate data used for case translation from the datatype package
Tue, 22 Jan 2013 13:32:41 +0100 berghofe case translations performed in a separate check phase (with adjustments by traytel)
Wed, 27 Mar 2013 10:55:05 +0100 haftmann centralized various multiset operations in theory multiset;
Tue, 26 Mar 2013 20:49:57 +0100 haftmann explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
Sat, 23 Mar 2013 20:50:39 +0100 haftmann fundamental revision of big operators on sets
Thu, 28 Feb 2013 17:14:55 +0100 wenzelm provide common HOLogic.conj_conv and HOLogic.eq_conv;
Thu, 28 Feb 2013 16:54:52 +0100 wenzelm just one HOLogic.Trueprop_conv, with regular exception CTERM;
Mon, 25 Feb 2013 12:17:50 +0100 wenzelm prefer stateless 'ML_val' for tests;
Sun, 17 Feb 2013 21:29:30 +0100 haftmann Sieve of Eratosthenes
Sun, 17 Feb 2013 11:34:40 +0100 haftmann simplified construction of upto_aux
Sat, 16 Feb 2013 15:27:10 +0100 nipkow tail recursive code for function "upto"
Fri, 15 Feb 2013 11:47:33 +0100 haftmann systematic conversions between nat and nibble/char;
Thu, 14 Feb 2013 12:24:42 +0100 haftmann abandoned theory Plain
Wed, 13 Feb 2013 13:38:52 +0100 haftmann combinator List.those;
Fri, 14 Dec 2012 19:51:20 +0100 nipkow unified layout of defs
Fri, 07 Dec 2012 16:25:33 +0100 wenzelm avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time) -- relevant for any application using it, e.g. small paper sessions;
Tue, 20 Nov 2012 18:59:35 +0100 hoelzl add Countable_Set theory
Thu, 08 Nov 2012 11:59:48 +0100 bulwahn adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs
Sun, 21 Oct 2012 17:04:13 +0200 webertj merged
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
less more (0) -300 -100 -60 tip