| Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
| Fri, 12 Aug 2016 17:53:55 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Wed, 13 Jul 2016 20:47:56 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Wed, 13 Jul 2016 14:28:15 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Thu, 05 Nov 2015 10:39:49 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Tue, 06 Oct 2015 15:14:28 +0200 |
wenzelm |
fewer aliases for toplevel theorem statements;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2015 22:57:34 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 17 Jun 2015 11:03:05 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:20:45 +0100 |
wenzelm |
modernized header;
|
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, 07 May 2014 14:44:07 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
| Thu, 12 Sep 2013 09:33:36 -0700 |
huffman |
new lemmas
|
file |
diff |
annotate
|
| Thu, 12 Apr 2012 23:15:34 +0200 |
krauss |
distributivity of * over Un and UNION
|
file |
diff |
annotate
|
| Thu, 12 Apr 2012 23:07:01 +0200 |
krauss |
Set_Algebras: removed syntax \<oplus> and \<otimes>, in favour of plain + and *
|
file |
diff |
annotate
|
| Thu, 12 Apr 2012 22:55:11 +0200 |
krauss |
removed "setsum_set", now subsumed by generic setsum
|
file |
diff |
annotate
|
| Thu, 12 Apr 2012 19:58:59 +0200 |
krauss |
backported Set_Algebras to use type classes (basically reverting b3e8d5ec721d from 2008)
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 18:02:16 -0700 |
huffman |
avoid warnings about duplicate rules
|
file |
diff |
annotate
|
| Thu, 02 Dec 2010 16:45:28 +0100 |
hoelzl |
Prove rel_interior_convex_hull_union (by Grechuck Bogdan).
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Fri, 20 Aug 2010 17:48:30 +0200 |
haftmann |
split and enriched theory SetsAndFunctions
|
file |
diff |
annotate
| base
|