| Sun, 11 Sep 2016 23:30:23 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sun, 11 Sep 2016 00:13:25 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 15:47:50 +0200 |
fleury |
add_mset constructor in multisets
|
file |
diff |
annotate
|
| Mon, 08 Aug 2016 17:47:51 +0200 |
eberlm |
is_prime -> prime
|
file |
diff |
annotate
|
| Wed, 20 Jul 2016 13:51:38 +0200 |
fleury |
adding mset_map to the simp rules
|
file |
diff |
annotate
|
| Thu, 26 May 2016 17:51:22 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Fri, 26 Feb 2016 22:44:11 +0100 |
haftmann |
more succint formulation of membership for multisets, similar to lists;
|
file |
diff |
annotate
|
| Sat, 10 Oct 2015 16:26:23 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Sun, 13 Sep 2015 22:56:52 +0200 |
wenzelm |
tuned proofs -- less legacy;
|
file |
diff |
annotate
|
| Fri, 19 Jun 2015 15:55:22 +0200 |
nipkow |
renamed multiset_of -> mset
|
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 13:24:16 +0200 |
Mathias Fleury |
Renaming multiset operators < ~> <#,...
|
file |
diff |
annotate
|
| Wed, 22 Apr 2015 12:11:48 +0200 |
nipkow |
added simp rules for ==>
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
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
|
| Tue, 05 Aug 2014 16:58:19 +0200 |
wenzelm |
tuned proofs -- fewer warnings;
|
file |
diff |
annotate
|
| Wed, 11 Jun 2014 14:24:23 +1000 |
Thomas Sewell |
Hypsubst preserves equality hypotheses
|
file |
diff |
annotate
|
| Sun, 02 Feb 2014 19:15:25 +0000 |
paulson |
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 01:12:40 +0200 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file |
diff |
annotate
|
| Thu, 08 Nov 2012 20:02:41 +0100 |
bulwahn |
tuned proofs
|
file |
diff |
annotate
|
| Fri, 06 Jan 2012 10:19:47 +0100 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 18:17:45 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 22:55:50 +0100 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 17:34:41 +0100 |
wenzelm |
explicit file specifications -- avoid secondary load path;
|
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
|
| Thu, 13 May 2010 14:34:05 +0200 |
nipkow |
Multiset: renamed, added and tuned lemmas;
|
file |
diff |
annotate
|
| Thu, 22 Apr 2010 20:39:48 +0100 |
paulson |
Tidied up using s/l
|
file |
diff |
annotate
|
| Sun, 21 Mar 2010 17:12:31 +0100 |
wenzelm |
standard headers;
|
file |
diff |
annotate
|
| Sun, 21 Mar 2010 16:51:37 +0100 |
wenzelm |
slightly more uniform definitions -- eliminated old-style meta-equality;
|
file |
diff |
annotate
|
| Sun, 21 Mar 2010 15:57:40 +0100 |
wenzelm |
eliminated old constdefs;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 13:40:23 +0100 |
haftmann |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file |
diff |
annotate
|
| Mon, 22 Feb 2010 09:15:10 +0100 |
haftmann |
switched notations for pointwise and multiset order
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Mon, 31 Aug 2009 14:09:42 +0200 |
nipkow |
tuned the simp rules for Int involving insert and intervals.
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 21:10:53 +0100 |
ballarin |
More porting to new locales.
|
file |
diff |
annotate
|
| Mon, 17 Nov 2008 17:00:55 +0100 |
haftmann |
tuned unfold_locales invocation
|
file |
diff |
annotate
|
| Wed, 15 Oct 2008 16:06:59 +0200 |
ballarin |
Removed 'includes' (fixed).
|
file |
diff |
annotate
|
| Wed, 15 Oct 2008 15:44:15 +0200 |
ballarin |
Removed 'includes'.
|
file |
diff |
annotate
|
| Fri, 01 Aug 2008 18:10:52 +0200 |
ballarin |
Generalised polynomial lemmas from cring to ring.
|
file |
diff |
annotate
|
| Wed, 30 Jul 2008 19:03:33 +0200 |
ballarin |
New locales for orders and lattices where the equivalence relation is not restricted to equality.
|
file |
diff |
annotate
|
| Tue, 29 Jul 2008 16:19:49 +0200 |
ballarin |
New theory on divisibility.
|
file |
diff |
annotate
|