src/HOL/List.thy
Thu, 10 Apr 2014 17:48:32 +0200 kuncar simplify and fix theories thanks to 356a5efdb278
Thu, 10 Apr 2014 17:48:15 +0200 kuncar abstract Domainp in relator_domain rules => more natural statement of the rule
Thu, 10 Apr 2014 17:48:15 +0200 kuncar more appropriate name (Lifting.invariant -> eq_onp)
Thu, 10 Apr 2014 17:48:14 +0200 kuncar left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
Fri, 21 Mar 2014 11:42:32 +0100 wenzelm more qualified names;
Wed, 19 Mar 2014 18:47:22 +0100 haftmann elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
Sun, 16 Mar 2014 18:09:04 +0100 haftmann normalising simp rules for compound operators
Thu, 13 Mar 2014 13:18:13 +0100 blanchet killed a few 'metis' calls
Thu, 06 Mar 2014 15:40:33 +0100 blanchet renamed 'fun_rel' to 'rel_fun'
Thu, 06 Mar 2014 15:29:18 +0100 blanchet renamed 'prod_rel' to 'rel_prod'
Thu, 06 Mar 2014 14:57:14 +0100 blanchet renamed 'set_rel' to 'rel_set'
Thu, 06 Mar 2014 13:36:48 +0100 blanchet renamed 'map_pair' to 'map_prod'
Fri, 28 Feb 2014 17:54:52 +0100 traytel load Metis a little later
Fri, 28 Feb 2014 18:09:37 +0100 nipkow added function "List.extract"
Fri, 21 Feb 2014 00:09:56 +0100 blanchet adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
Wed, 19 Feb 2014 16:32:37 +0100 blanchet merged 'List.set' with BNF-generated 'set'
Tue, 18 Feb 2014 23:03:49 +0100 kuncar delete or move now not necessary reflexivity rules due to 1726f46d2aa8
Mon, 17 Feb 2014 13:31:42 +0100 blanchet renamed 'datatype_new_compat' to 'datatype_compat'
Sun, 16 Feb 2014 21:33:28 +0100 blanchet folded 'rel_option' into 'option_rel'
Sun, 16 Feb 2014 21:33:28 +0100 blanchet folded 'list_all2' with the relator generated by 'datatype_new'
Fri, 14 Feb 2014 07:53:46 +0100 blanchet hide 'rel' name -- this one is waiting to be merged with 'list_all2'
Fri, 14 Feb 2014 07:53:46 +0100 blanchet renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
Fri, 14 Feb 2014 07:53:46 +0100 blanchet merged 'Option.map' and 'Option.map_option'
Fri, 14 Feb 2014 07:53:45 +0100 blanchet merged 'List.map' and 'List.list.map'
Wed, 12 Feb 2014 17:35:59 +0100 blanchet tuning
Wed, 12 Feb 2014 08:37:06 +0100 blanchet adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed 'nat_{case,rec}' to '{case,rec}_nat'
Wed, 12 Feb 2014 08:35:56 +0100 blanchet compatibility names
Wed, 12 Feb 2014 08:35:56 +0100 blanchet use new selector support to define 'the', 'hd', 'tl'
Wed, 12 Feb 2014 08:35:56 +0100 blanchet transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well)
Sat, 25 Jan 2014 23:50:49 +0100 haftmann avoid (now superfluous) indirect passing of constant names
Sat, 25 Jan 2014 23:50:49 +0100 haftmann prefer explicit code symbol type over ad-hoc name mangling
Fri, 24 Jan 2014 11:51:45 +0100 blanchet killed 'More_BNFs' by moving its various bits where they (now) belong
Wed, 01 Jan 2014 01:05:48 +0100 haftmann fundamental treatment of undefined vs. universally partial replaces code_abort
Tue, 31 Dec 2013 22:18:31 +0100 haftmann more abstract declaration of code attributes
Fri, 27 Dec 2013 14:35:14 +0100 haftmann prefer target-style syntaxx for sublocale
Wed, 25 Dec 2013 17:39:06 +0100 haftmann prefer more canonical names for lemmas on min/max
Wed, 27 Nov 2013 11:08:55 +0100 Andreas Lochbihler remove junk
Wed, 27 Nov 2013 10:43:51 +0100 Andreas Lochbihler merged
Wed, 20 Nov 2013 10:59:12 +0100 Andreas Lochbihler add predicate version of lexicographic order on lists
Thu, 21 Nov 2013 21:33:34 +0100 blanchet rationalize imports
Tue, 19 Nov 2013 17:07:52 +0100 hoelzl merged
Mon, 18 Nov 2013 17:14:01 +0100 hoelzl add lemmas Suc_funpow and id_funpow to simpset; add lemma map_add_upt
Tue, 19 Nov 2013 10:05:53 +0100 haftmann eliminiated neg_numeral in favour of - (numeral _)
Tue, 12 Nov 2013 13:47:24 +0100 blanchet port list comprehension simproc to 'Ctr_Sugar' abstraction
Sun, 10 Nov 2013 15:05:06 +0100 haftmann qualifed popular user space names
Fri, 18 Oct 2013 10:43:20 +0200 blanchet killed most "no_atp", to make Sledgehammer more complete
Fri, 27 Sep 2013 15:38:23 +0200 nipkow added code eqns for bounded LEAST operator
Thu, 26 Sep 2013 13:37:33 +0200 lammich Added symmetric code_unfold-lemmas for null and is_none
Wed, 18 Sep 2013 18:11:32 +0200 traytel added two functions to List (one contributed by Manuel Eberl)
Wed, 18 Sep 2013 12:16:10 +0200 nipkow added and tuned lemmas
Thu, 05 Sep 2013 11:10:51 +0200 traytel list_to_set_comprehension: don't crash in case distinctions on datatypes with even number of constructors
Tue, 03 Sep 2013 01:12:40 +0200 wenzelm tuned proofs -- clarified flow of facts wrt. calculation;
Tue, 13 Aug 2013 17:45:22 +0200 wenzelm merged
Tue, 13 Aug 2013 16:25:47 +0200 wenzelm standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
Tue, 13 Aug 2013 15:59:22 +0200 kuncar move Lifting/Transfer relevant parts of Library/Quotient_* to Main
Sun, 23 Jun 2013 21:16:07 +0200 haftmann migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
Sat, 15 Jun 2013 17:19:23 +0200 haftmann lifting for primitive definitions;
Sat, 15 Jun 2013 17:19:23 +0200 haftmann selection operator smallest_prime_beyond
Sat, 25 May 2013 18:30:38 +0200 wenzelm merged
less more (0) -300 -100 -60 tip