| Mon, 17 Oct 2016 17:33:07 +0200 |
nipkow |
setprod -> prod
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
| Fri, 16 Sep 2016 21:28:09 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Sun, 11 Sep 2016 00:14:44 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 24 Aug 2016 11:02:23 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Wed, 10 Aug 2016 18:57:20 +0200 |
haftmann |
lists form a monoid
|
file |
diff |
annotate
|
| Fri, 29 Jul 2016 09:49:23 +0200 |
Andreas Lochbihler |
add lemmas contributed by Peter Gammie
|
file |
diff |
annotate
|
| Fri, 22 Jul 2016 11:00:43 +0200 |
wenzelm |
tuned proofs -- avoid unstructured calculation;
|
file |
diff |
annotate
|
| Tue, 19 Jul 2016 14:09:55 +0200 |
Lars Hupel |
added missing transfer rule
|
file |
diff |
annotate
|
| Sat, 02 Jul 2016 08:41:05 +0200 |
haftmann |
more theorems
|
file |
diff |
annotate
|
| Wed, 22 Jun 2016 10:09:20 +0200 |
wenzelm |
bundle lifting_syntax;
|
file |
diff |
annotate
|
| Thu, 16 Jun 2016 17:57:09 +0200 |
eberlm |
Various additions to polynomials, FPSs, Gamma function
|
file |
diff |
annotate
|
| Sun, 29 May 2016 14:10:48 +0200 |
nipkow |
added subtheory of longest common prefix
|
file |
diff |
annotate
|
| Wed, 25 May 2016 11:49:40 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Tue, 17 May 2016 17:05:35 +0200 |
eberlm |
Moved material from AFP/Randomised_Social_Choice to distribution
|
file |
diff |
annotate
|
| Fri, 13 May 2016 20:24:10 +0200 |
wenzelm |
eliminated use of empty "assms";
|
file |
diff |
annotate
|
| Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
| Thu, 10 Mar 2016 12:33:01 +0100 |
haftmann |
moved
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:56 +0100 |
haftmann |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 11:39:26 +0100 |
traytel |
call the predicator of list list_all
|
file |
diff |
annotate
|
| Wed, 13 Jan 2016 23:07:06 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Fri, 08 Jan 2016 16:37:56 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 07 Jan 2016 15:53:39 +0100 |
wenzelm |
more uniform treatment of package internals;
|
file |
diff |
annotate
|
| 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
|
| Fri, 30 May 2014 12:27:51 +0200 |
blanchet |
tuned whitespace, to make datatype definitions slightly less intimidating
|
file |
diff |
annotate
|
| Mon, 26 May 2014 16:32:55 +0200 |
blanchet |
got rid of '=:' squiggly
|
file |
diff |
annotate
|
| Wed, 14 May 2014 11:33:38 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Tue, 29 Apr 2014 16:02:02 +0200 |
wenzelm |
prefer plain ASCII / latex over not-so-universal Unicode;
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
move size hooks together, with new one preceding old one and sharing same theory data
|
file |
diff |
annotate
|
| Sat, 12 Apr 2014 11:27:36 +0200 |
haftmann |
more operations and lemmas
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:54 +0200 |
kuncar |
make list_all an abbreviation of pred_list - prevent duplication
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:32 +0200 |
kuncar |
simplify and fix theories thanks to 356a5efdb278
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:15 +0200 |
kuncar |
abstract Domainp in relator_domain rules => more natural statement of the rule
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:15 +0200 |
kuncar |
more appropriate name (Lifting.invariant -> eq_onp)
|
file |
diff |
annotate
|
| 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)
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 11:42:32 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Sun, 16 Mar 2014 18:09:04 +0100 |
haftmann |
normalising simp rules for compound operators
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 13:18:13 +0100 |
blanchet |
killed a few 'metis' calls
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:40:33 +0100 |
blanchet |
renamed 'fun_rel' to 'rel_fun'
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:29:18 +0100 |
blanchet |
renamed 'prod_rel' to 'rel_prod'
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 14:57:14 +0100 |
blanchet |
renamed 'set_rel' to 'rel_set'
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 13:36:48 +0100 |
blanchet |
renamed 'map_pair' to 'map_prod'
|
file |
diff |
annotate
|
| Fri, 28 Feb 2014 17:54:52 +0100 |
traytel |
load Metis a little later
|
file |
diff |
annotate
|
| Fri, 28 Feb 2014 18:09:37 +0100 |
nipkow |
added function "List.extract"
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 00:09:56 +0100 |
blanchet |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 16:32:37 +0100 |
blanchet |
merged 'List.set' with BNF-generated 'set'
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 23:03:49 +0100 |
kuncar |
delete or move now not necessary reflexivity rules due to 1726f46d2aa8
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 13:31:42 +0100 |
blanchet |
renamed 'datatype_new_compat' to 'datatype_compat'
|
file |
diff |
annotate
|
| Sun, 16 Feb 2014 21:33:28 +0100 |
blanchet |
folded 'rel_option' into 'option_rel'
|
file |
diff |
annotate
|
| Sun, 16 Feb 2014 21:33:28 +0100 |
blanchet |
folded 'list_all2' with the relator generated by 'datatype_new'
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 07:53:46 +0100 |
blanchet |
hide 'rel' name -- this one is waiting to be merged with 'list_all2'
|
file |
diff |
annotate
|
| 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)
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 07:53:46 +0100 |
blanchet |
merged 'Option.map' and 'Option.map_option'
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 07:53:45 +0100 |
blanchet |
merged 'List.map' and 'List.list.map'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 17:35:59 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed 'nat_{case,rec}' to '{case,rec}_nat'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
compatibility names
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
use new selector support to define 'the', 'hd', 'tl'
|
file |
diff |
annotate
|