| Sun, 13 Sep 2015 22:56:52 +0200 | wenzelm | tuned proofs -- less legacy; | file | diff | annotate |
| Tue, 01 Sep 2015 22:32:58 +0200 | wenzelm | eliminated \<Colon>; | file | diff | annotate |
| Thu, 27 Aug 2015 21:19:48 +0200 | haftmann | standardized some occurences of ancient "split" alias | file | diff | annotate |
| Thu, 27 Aug 2015 13:07:45 +0200 | haftmann | more lemmas on sorting and multisets (due to Thomas Sewell) | file | diff | annotate |
| Sat, 18 Jul 2015 22:58:50 +0200 | wenzelm | isabelle update_cartouches; | file | diff | annotate |
| Sat, 18 Jul 2015 20:47:08 +0200 | wenzelm | prefer tactics with explicit context; | file | diff | annotate |
| Thu, 25 Jun 2015 23:33:47 +0200 | wenzelm | tuned proofs; | file | diff | annotate |
| Mon, 22 Jun 2015 11:15:23 +0200 | nipkow | modernized name | file | diff | annotate |
| Thu, 30 Apr 2015 16:07:43 +0200 | wenzelm | more formal source, more PIDE markup; | file | diff | annotate |
| Thu, 30 Apr 2015 15:58:15 +0200 | wenzelm | tuned -- avoid odd rebinding of "ctxt" and "context"; | file | diff | annotate |
| Thu, 30 Apr 2015 15:41:53 +0200 | wenzelm | tuned; | file | diff | annotate |
| Wed, 29 Apr 2015 23:26:11 +0200 | wenzelm | tuned; | file | diff | annotate |
| Tue, 17 Mar 2015 09:22:17 +0100 | nipkow | added lemmas | file | diff | annotate |
| Wed, 04 Mar 2015 19:53:18 +0100 | wenzelm | tuned signature -- prefer qualified names; | file | diff | annotate |
| Wed, 11 Feb 2015 13:58:51 +0100 | Andreas Lochbihler | add parametricity rules for monotone, fun_lub, and fun_ord | file | diff | annotate |
| Mon, 29 Dec 2014 21:02:49 +0100 | wenzelm | tuned; | file | diff | annotate |
| Tue, 11 Nov 2014 14:46:26 +0100 | noschinl | added lemma | file | diff | annotate |
| Mon, 10 Nov 2014 10:29:19 +0100 | traytel | dropped redundant transfer rules (now proved and registered by datatype and plugins) | file | diff | annotate |
| Sun, 09 Nov 2014 14:08:00 +0100 | wenzelm | proper context for compose_tac, Splitter.split_tac (relevant for unify trace options); | file | diff | annotate |
| Fri, 07 Nov 2014 11:28:37 +0100 | traytel | more complete fp_sugars for sum and prod; | file | diff | annotate |
| Sun, 02 Nov 2014 18:21:45 +0100 | wenzelm | modernized header uniformly as section; | file | diff | annotate |
| Wed, 29 Oct 2014 12:01:39 +0100 | nipkow | removed useless lemmas | file | diff | annotate |
| Wed, 29 Oct 2014 11:03:23 +0100 | nipkow | tuned layout and proofs | file | diff | annotate |
| Wed, 24 Sep 2014 19:11:21 +0200 | haftmann | added lemmas | file | diff | annotate |
| Thu, 11 Sep 2014 19:32:36 +0200 | blanchet | updated news | file | diff | annotate |
| Tue, 09 Sep 2014 17:50:54 +0200 | nipkow | enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc | file | diff | annotate |
| Sat, 06 Sep 2014 20:12:32 +0200 | haftmann | added various facts | file | diff | annotate |
| Tue, 02 Sep 2014 09:28:23 +0200 | traytel | silenced nonexhaustive primrec warnings | file | diff | annotate |
| Sun, 31 Aug 2014 09:10:42 +0200 | haftmann | separated listsum material | file | diff | annotate |
| Mon, 25 Aug 2014 16:06:41 +0200 | nipkow | added lemmas | file | diff | annotate |