NEWS
Tue, 06 Sep 2011 07:48:59 -0700 huffman remove redundant lemma real_sum_squared_expand in favor of power2_sum
Tue, 06 Sep 2011 07:45:18 -0700 huffman remove redundant lemma LIMSEQ_Complex in favor of tendsto_Complex
Sun, 04 Sep 2011 10:05:52 -0700 huffman remove redundant lemmas expi_add and expi_zero
Sun, 04 Sep 2011 09:49:45 -0700 huffman remove redundant lemmas about LIMSEQ
Sat, 03 Sep 2011 09:26:11 -0700 huffman remove duplicate lemma finite_choice in favor of finite_set_choice
Fri, 02 Sep 2011 16:48:30 -0700 huffman remove redundant lemma reals_complete2 in favor of complete_real
Fri, 02 Sep 2011 13:57:12 -0700 huffman remove more duplicate lemmas
Thu, 01 Sep 2011 10:41:19 -0700 huffman simplify some proofs about uniform continuity, and add some new ones;
Thu, 01 Sep 2011 09:02:14 -0700 huffman modernize lemmas about 'continuous' and 'continuous_on';
Sun, 28 Aug 2011 09:20:12 -0700 huffman discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
Fri, 26 Aug 2011 15:11:26 -0700 huffman NEWS entry for setsum_norm ~> norm_setsum
Thu, 25 Aug 2011 19:41:38 -0700 huffman replace some continuous_on lemmas with more general versions
Thu, 25 Aug 2011 16:50:55 -0700 huffman remove legacy theorem Lim_inner
Thu, 25 Aug 2011 15:35:54 -0700 huffman remove dot_lsum and dot_rsum in favor of inner_setsum_{left,right}
Thu, 25 Aug 2011 12:43:55 -0700 huffman rename subset_{interior,closure} to {interior,closure}_mono;
Fri, 19 Aug 2011 19:33:31 +0200 haftmann more concise definition for Inf, Sup on bool
Thu, 18 Aug 2011 13:36:58 -0700 huffman remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
Thu, 18 Aug 2011 17:42:18 +0200 nipkow case_names NEWS
Wed, 10 Aug 2011 13:13:37 -0700 huffman more uniform naming scheme for finite cartesian product type and related theorems
Tue, 09 Aug 2011 08:06:15 +0200 haftmann more uniform naming scheme for Inf/INF and Sup/SUP lemmas
Tue, 09 Aug 2011 07:44:17 +0200 haftmann merged
Mon, 08 Aug 2011 19:21:11 +0200 haftmann dropped lemmas (Inf|Sup)_(singleton|binary)
Mon, 08 Aug 2011 19:26:53 -0700 huffman rename type 'a net to 'a filter, following standard mathematical terminology
Thu, 04 Aug 2011 07:31:43 +0200 haftmann NEWS
Wed, 03 Aug 2011 16:08:02 +0200 bulwahn NEWS
Tue, 02 Aug 2011 08:28:34 -0700 huffman Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
Tue, 02 Aug 2011 07:36:58 -0700 huffman NEWS: fix typo
Tue, 02 Aug 2011 12:17:48 +0200 krauss NEWS
Mon, 25 Jul 2011 23:27:20 +0200 haftmann merged
Sun, 24 Jul 2011 21:27:25 +0200 haftmann more coherent structure in and across theories
Mon, 25 Jul 2011 10:42:32 +0200 bulwahn NEWS
Wed, 20 Jul 2011 22:14:39 +0200 haftmann class complete_linorder
Mon, 18 Jul 2011 21:34:01 +0200 haftmann avoid misunderstandable names
Sun, 17 Jul 2011 22:24:08 +0200 haftmann more on complement
Sun, 17 Jul 2011 20:57:56 +0200 haftmann more consistent theorem names
Sun, 17 Jul 2011 15:15:58 +0200 haftmann further generalization from sets to complete lattices
Wed, 13 Jul 2011 23:49:56 +0200 haftmann uniqueness lemmas for bot and top
Wed, 13 Jul 2011 23:41:13 +0200 haftmann adjusted to tightened specification of classes bot and top
Mon, 11 Jul 2011 17:22:15 +0200 wenzelm NEWS;
Sun, 10 Jul 2011 21:46:41 +0200 wenzelm merged;
Sun, 10 Jul 2011 14:02:27 +0200 bulwahn improved NEWS
Sat, 09 Jul 2011 21:18:20 +0200 bulwahn NEWS
Sun, 10 Jul 2011 20:59:04 +0200 wenzelm inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
Fri, 08 Jul 2011 16:13:34 +0200 wenzelm discontinued special treatment of hard tabulators;
Fri, 01 Jul 2011 15:53:38 +0200 blanchet update documentation after "type_enc" renaming + fixed a few other out-of-date factlets
Fri, 01 Jul 2011 10:45:51 +0200 bulwahn adding a minimalistic documentation of the value antiquotation in the Isar reference manual
Mon, 27 Jun 2011 22:44:44 +0200 wenzelm merged
Mon, 27 Jun 2011 14:56:29 +0200 blanchet minor Sledgehammer news
Mon, 27 Jun 2011 14:56:10 +0200 blanchet document changes to Sledgehammer and "try"
Mon, 27 Jun 2011 22:23:44 +0200 wenzelm NEWS;
Thu, 23 Jun 2011 12:02:54 +0200 ballarin Release notes should be written from the user's perspective. Don't assume the user has universal knowledge of the system.
Thu, 09 Jun 2011 10:43:42 +0200 bulwahn NEWS
Tue, 07 Jun 2011 08:52:35 +0200 blanchet obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
Mon, 06 Jun 2011 20:36:35 +0200 blanchet marked "metisF" as legacy -- nobody uses it or needs it
Fri, 20 May 2011 20:44:03 +0200 wenzelm added Isabelle_Process.is_active;
Fri, 20 May 2011 12:09:54 +0200 haftmann NEWS
Wed, 18 May 2011 15:45:34 +0200 bulwahn NEWS
Sun, 15 May 2011 18:00:08 +0200 wenzelm NEWS (cf. 4e8483cc2cc5);
Sat, 14 May 2011 18:26:25 +0200 haftmann use pointfree characterisation for fold_set locale
Fri, 13 May 2011 22:55:00 +0200 wenzelm proper Proof.context for classical tactics;
less more (0) -1000 -300 -100 -60 tip