src/HOL/List.thy
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
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
less more (0) -300 -100 -60 tip