src/HOL/List.thy
Tue, 13 Sep 2011 12:14:29 +0200 bulwahn added lemma motivated by a more specific lemma in the AFP-KBPs theories
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Thu, 01 Sep 2011 13:18:27 +0200 blanchet added two lemmas about "distinct" to help Sledgehammer
Tue, 30 Aug 2011 20:10:48 +0200 bulwahn adding list_size_append (thanks to Rene Thiemann)
Tue, 30 Aug 2011 20:10:47 +0200 bulwahn strengthening list_size_pointwise (thanks to Rene Thiemann)
Fri, 26 Aug 2011 11:22:47 +0200 nipkow added lemma
Tue, 02 Aug 2011 10:36:50 +0200 krauss moved recdef package to HOL/Library/Old_Recdef.thy
Wed, 29 Jun 2011 17:35:46 +0200 wenzelm modernized some simproc setup;
Mon, 27 Jun 2011 17:04:04 +0200 krauss new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor;
Thu, 09 Jun 2011 16:34:49 +0200 wenzelm discontinued Name.variant to emphasize that this is old-style / indirect;
Fri, 20 May 2011 11:44:16 +0200 haftmann names of fold_set locales resemble name of characteristic property more closely
Sat, 14 May 2011 18:26:25 +0200 haftmann use pointfree characterisation for fold_set locale
Mon, 09 May 2011 16:11:20 +0200 noschinl add a lemma about commutative append to List.thy
Mon, 09 May 2011 12:26:25 +0200 noschinl removed assumption from lemma List.take_add
Tue, 19 Apr 2011 23:57:28 +0200 wenzelm eliminated Codegen.mode in favour of explicit argument;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Sat, 16 Apr 2011 15:25:25 +0200 wenzelm prefer local name spaces;
Wed, 06 Apr 2011 23:04:00 +0200 wenzelm separate structure Term_Position;
Wed, 30 Mar 2011 20:19:21 +0200 wenzelm actually check list comprehension examples;
Mon, 28 Mar 2011 23:49:53 +0200 wenzelm list comprehension: strip positions where the translation cannot handle them right now;
Tue, 22 Mar 2011 20:44:47 +0100 wenzelm more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
Tue, 15 Mar 2011 22:04:02 +0100 nipkow added lemma
Fri, 25 Feb 2011 14:25:41 +0100 nipkow added simp lemma nth_Cons_pos to List
Thu, 03 Feb 2011 18:57:42 +0100 wenzelm explicit is better than implicit;
Tue, 11 Jan 2011 14:12:37 +0100 haftmann "enriched_type" replaces less specific "type_lifting"
Fri, 07 Jan 2011 18:10:35 +0100 bulwahn adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
Tue, 21 Dec 2010 17:52:23 +0100 haftmann tuned type_lifting declarations
Fri, 17 Dec 2010 17:43:54 +0100 wenzelm replaced command 'nonterminals' by slightly modernized version 'nonterminal';
Wed, 08 Dec 2010 13:34:50 +0100 haftmann primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
Mon, 06 Dec 2010 09:19:10 +0100 haftmann replace `type_mapper` by the more adequate `type_lifting`
Sun, 28 Nov 2010 15:20:51 +0100 nipkow gave more standard finite set rules simp and intro attribute
Mon, 22 Nov 2010 11:34:58 +0100 bulwahn adding code equations for EX1 on finite types
Thu, 18 Nov 2010 17:01:16 +0100 haftmann mapper for list type; map_pair replaces prod_fun
Wed, 17 Nov 2010 21:35:23 +0100 nipkow code eqn for slice was missing; redefined splice with fun
Fri, 05 Nov 2010 08:16:34 +0100 bulwahn added two lemmas about injectivity of concat to the list theory
Tue, 02 Nov 2010 16:31:57 +0100 haftmann lemmas sorted_map_same, sorted_same
Thu, 28 Oct 2010 17:54:09 +0200 nipkow added lemmas about listrel(1)
Wed, 27 Oct 2010 16:40:31 +0200 haftmann sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas
Tue, 26 Oct 2010 16:39:21 +0200 haftmann include ATP in theory List -- avoid theory edge by-passing the prominent list theory
Mon, 25 Oct 2010 13:34:58 +0200 haftmann dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps
Sun, 24 Oct 2010 20:19:00 +0200 nipkow nat_number -> eval_nat_numeral
Wed, 06 Oct 2010 17:44:21 +0200 blanchet merged
Mon, 04 Oct 2010 22:45:09 +0200 blanchet move Metis into Plain
Mon, 04 Oct 2010 12:22:58 +0200 haftmann turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
Tue, 28 Sep 2010 15:21:45 +0200 haftmann localized listsum
Mon, 27 Sep 2010 14:13:22 +0200 haftmann lemma remdups_map_remdups
Wed, 22 Sep 2010 16:52:09 +0200 nipkow more lists lemmas
Tue, 21 Sep 2010 02:03:40 +0200 nipkow new lemma
Fri, 17 Sep 2010 20:53:50 +0200 haftmann generalized lemma insort_remove1 to insort_key_remove1
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Fri, 10 Sep 2010 10:21:25 +0200 haftmann Haskell == is infix, not infixl
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Thu, 02 Sep 2010 10:18:15 +0200 hoelzl Add filter_remove1
Fri, 27 Aug 2010 19:34:23 +0200 haftmann renamed class/constant eq to equal; tuned some instantiations
Wed, 25 Aug 2010 18:36:22 +0200 wenzelm renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
Mon, 19 Jul 2010 11:55:43 +0200 haftmann Scala: subtle difference in printing strings vs. complex mixfix syntax
Mon, 12 Jul 2010 10:48:37 +0200 haftmann dropped superfluous [code del]s
Mon, 28 Jun 2010 15:32:26 +0200 haftmann put section on distinctness before listsum; refined code generation operations; dropped ancient infix mem
Fri, 18 Jun 2010 21:22:05 +0200 haftmann merged
Fri, 18 Jun 2010 09:21:41 +0200 haftmann made List.thy a join point in the theory graph
less more (0) -300 -100 -60 tip