| Fri, 08 Jan 2016 16:36:41 +0100 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Tue, 05 Jan 2016 17:54:10 +0100 |
eberlm |
Added some facts about polynomials
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 21:47:32 +0100 |
wenzelm |
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
|
file |
diff |
annotate
|
| Sun, 27 Dec 2015 17:16:21 +0100 |
wenzelm |
discontinued ASCII replacement syntax <->;
|
file |
diff |
annotate
|
| Thu, 10 Dec 2015 13:38:40 +0000 |
paulson |
not_leE -> not_le_imp_less and other tidying
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Wed, 18 Nov 2015 15:23:34 +0000 |
paulson |
New theorems mostly from Peter Gammie
|
file |
diff |
annotate
|
| Sun, 15 Nov 2015 13:49:27 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Sun, 15 Nov 2015 12:39:51 +0100 |
wenzelm |
option "inductive_defs" controls exposure of def and mono facts;
|
file |
diff |
annotate
|
| Sat, 14 Nov 2015 08:45:51 +0100 |
haftmann |
reverted half-baken 7d1127ac2251
|
file |
diff |
annotate
|
| Wed, 11 Nov 2015 09:48:24 +0100 |
Andreas Lochbihler |
add various lemmas
|
file |
diff |
annotate
|
| Mon, 09 Nov 2015 15:48:17 +0100 |
wenzelm |
qualifier is mandatory by default;
|
file |
diff |
annotate
|
| Wed, 04 Nov 2015 08:13:52 +0100 |
ballarin |
Keyword 'rewrites' identifies rewrite morphisms.
|
file |
diff |
annotate
|
| Sat, 17 Oct 2015 16:08:30 +0200 |
haftmann |
code abbreviation for mapping over a fixed range
|
file |
diff |
annotate
|
| Fri, 09 Oct 2015 20:26:03 +0200 |
wenzelm |
discontinued specific HTML syntax;
|
file |
diff |
annotate
|
| 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
|
| Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
|
file |
diff |
annotate
|
| Mon, 21 Jul 2014 17:51:29 +0200 |
Andreas Lochbihler |
add parametricity lemmas
|
file |
diff |
annotate
|
| Sat, 19 Jul 2014 18:30:43 +0200 |
haftmann |
reverse induction over nonempty lists
|
file |
diff |
annotate
|
| Wed, 09 Jul 2014 11:48:21 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Sat, 05 Jul 2014 11:01:53 +0200 |
haftmann |
prefer ac_simps collections over separate name bindings for add and mult
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| Sat, 28 Jun 2014 09:16:42 +0200 |
haftmann |
fact consolidation
|
file |
diff |
annotate
|
| Tue, 24 Jun 2014 15:05:58 +0200 |
Andreas Lochbihler |
add lemma
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 18:47:27 +0200 |
nipkow |
merged
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 18:47:16 +0200 |
nipkow |
added [simp]
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 17:02:03 +0200 |
blanchet |
reintroduced vital 'Thm.transfer'
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 01:00:49 +0200 |
blanchet |
reduces Sledgehammer dependencies
|
file |
diff |
annotate
|
| Tue, 10 Jun 2014 21:15:57 +0200 |
blanchet |
changed syntax of map: and rel: arguments to BNF-based datatypes
|
file |
diff |
annotate
|
| Tue, 10 Jun 2014 12:16:22 +0200 |
blanchet |
use 'where' clause for selector default value syntax
|
file |
diff |
annotate
|
| Mon, 09 Jun 2014 16:08:30 +0200 |
nipkow |
added List.union
|
file |
diff |
annotate
|