| Thu, 05 Nov 2015 10:39:49 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Wed, 04 Nov 2015 08:13:52 +0100 |
ballarin |
Keyword 'rewrites' identifies rewrite morphisms.
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
| Fri, 09 Oct 2015 20:26:03 +0200 |
wenzelm |
discontinued specific HTML syntax;
|
file |
diff |
annotate
|
| Tue, 06 Oct 2015 17:44:32 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Tue, 06 Oct 2015 15:14:28 +0200 |
wenzelm |
fewer aliases for toplevel theorem statements;
|
file |
diff |
annotate
|
| Tue, 06 Oct 2015 11:50:23 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
| Thu, 17 Sep 2015 15:47:24 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
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
|
| Mon, 27 Jul 2015 22:44:02 +0200 |
haftmann |
formal class for factorial (semi)rings
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 20:47:08 +0200 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2015 22:06:02 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 30 Jun 2015 13:29:30 +0200 |
hoelzl |
fix tex-output for rel_mset
|
file |
diff |
annotate
|
| Mon, 29 Jun 2015 16:07:55 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Mon, 29 Jun 2015 15:41:16 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Mon, 29 Jun 2015 15:36:29 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Fri, 19 Jun 2015 15:55:22 +0200 |
nipkow |
renamed multiset_of -> mset
|
file |
diff |
annotate
|
| Thu, 18 Jun 2015 16:16:17 +0200 |
nipkow |
multiset_of_set -> mset_set
|
file |
diff |
annotate
|
| Wed, 17 Jun 2015 18:22:29 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 17 Jun 2015 17:54:09 +0200 |
wenzelm |
manual merge;
|
file |
diff |
annotate
|
| Wed, 17 Jun 2015 11:03:05 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Wed, 17 Jun 2015 18:13:44 +0200 |
nipkow |
more compact name
|
file |
diff |
annotate
|
| Wed, 17 Jun 2015 17:21:11 +0200 |
nipkow |
renamed Multiset.set_of to the canonical set_mset
|
file |
diff |
annotate
|
| Wed, 10 Jun 2015 15:50:17 +0200 |
fleury |
tuned
|
file |
diff |
annotate
|
| Wed, 10 Jun 2015 13:24:16 +0200 |
Mathias Fleury |
Renaming multiset operators < ~> <#,...
|
file |
diff |
annotate
|
| Fri, 10 Apr 2015 12:16:58 +0200 |
nipkow |
merged
|
file |
diff |
annotate
|
| Fri, 10 Apr 2015 12:16:45 +0200 |
nipkow |
renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset
|
file |
diff |
annotate
|
| Fri, 10 Apr 2015 11:52:55 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Thu, 09 Apr 2015 18:00:58 +0200 |
blanchet |
introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 15:21:20 +0200 |
blanchet |
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
|
file |
diff |
annotate
|
| Tue, 07 Apr 2015 18:21:56 +0200 |
nipkow |
Removed mcard because it is equal to size
|
file |
diff |
annotate
|
| Mon, 23 Mar 2015 19:05:14 +0100 |
haftmann |
explicit commutative additive inverse operation;
|
file |
diff |
annotate
|
| Wed, 25 Mar 2015 17:51:34 +0100 |
blanchet |
more multiset theorems
|
file |
diff |
annotate
|
| Wed, 25 Mar 2015 10:44:57 +0100 |
wenzelm |
prefer local fixes;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 20:08:45 +0100 |
wenzelm |
proper context;
|
file |
diff |
annotate
|
| Thu, 19 Feb 2015 11:53:36 +0100 |
haftmann |
establish unique preferred fact names
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:20:45 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Wed, 24 Sep 2014 15:45:55 +0200 |
blanchet |
simpler proof
|
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, 30 Aug 2014 11:15:47 +0200 |
haftmann |
inlined unused definition
|
file |
diff |
annotate
|
| Fri, 22 Aug 2014 17:35:48 +0200 |
blanchet |
added lemmas contributed by Rene Thiemann
|
file |
diff |
annotate
|
| Sun, 17 Aug 2014 22:27:58 +0200 |
blanchet |
use 'image_mset' as BNF map function
|
file |
diff |
annotate
|
| Sat, 05 Jul 2014 16:04:23 +0200 |
haftmann |
refrain from auxiliary abbreviation: be more explicit to the reader in situations where syntax translation does not apply;
|
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
|
| Wed, 11 Jun 2014 14:24:23 +1000 |
Thomas Sewell |
Hypsubst preserves equality hypotheses
|
file |
diff |
annotate
|
| Sat, 28 Jun 2014 09:16:42 +0200 |
haftmann |
fact consolidation
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
size function for multisets
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:40:33 +0100 |
blanchet |
renamed 'fun_rel' to 'rel_fun'
|
file |
diff |
annotate
|
| Wed, 05 Mar 2014 09:59:48 +0100 |
wenzelm |
proper UTF-8;
|
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:11:02 +0100 |
nipkow |
added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 23:03:50 +0100 |
kuncar |
simplify proofs because of the stronger reflexivity prover
|
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
|
| 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
|
| Fri, 24 Jan 2014 11:51:45 +0100 |
blanchet |
killed 'More_BNFs' by moving its various bits where they (now) belong
|
file |
diff |
annotate
|
| Fri, 27 Dec 2013 14:35:14 +0100 |
haftmann |
prefer target-style syntaxx for sublocale
|
file |
diff |
annotate
|
| Sun, 10 Nov 2013 15:05:06 +0100 |
haftmann |
qualifed popular user space names
|
file |
diff |
annotate
|
| Sun, 02 Jun 2013 20:44:55 +0200 |
haftmann |
type class for confined subtraction
|
file |
diff |
annotate
|