| Wed, 17 Feb 2016 21:51:57 +0100 |
haftmann |
dropped various legacy fact bindings
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 01:28:28 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Wed, 04 Nov 2015 08:13:52 +0100 |
ballarin |
Keyword 'rewrites' identifies rewrite morphisms.
|
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, 17 Apr 2015 11:52:36 +0200 |
Rene Thiemann |
finprod takes 1 in case of infinite sets => remove several "finite A" assumptions
|
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
|
| Fri, 07 Mar 2014 23:28:05 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 05 Mar 2014 21:51:30 +0100 |
wenzelm |
more symbols;
|
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
|
| Mon, 27 Jan 2014 16:38:52 +0000 |
paulson |
converting to new Number_Theory
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 09:02:58 -0700 |
huffman |
avoid using legacy theorem names
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 18:17:45 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Thu, 06 Jan 2011 21:06:17 +0100 |
ballarin |
Abelian group facts obtained from group facts via interpretation (sublocale).
|
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
|
| 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
|
| Fri, 13 Nov 2009 22:01:01 +0100 |
nipkow |
moved lemma from Algebra/IntRing to Ring_and_Field
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 14:14:04 +0100 |
nipkow |
renamed lemmas "anti_sym" -> "antisym"
|
file |
diff |
annotate
|
| Tue, 01 Sep 2009 16:00:57 +0200 |
haftmann |
some reorganization of number theory
|
file |
diff |
annotate
|
| Thu, 26 Mar 2009 20:08:55 +0100 |
wenzelm |
interpretation/interpret: prefixes are mandatory by default;
|
file |
diff |
annotate
|
| Tue, 17 Feb 2009 18:48:17 +0100 |
nipkow |
Cleaned up IntDiv and removed subsumed lemmas.
|
file |
diff |
annotate
|
| Sat, 31 Jan 2009 09:04:16 +0100 |
nipkow |
added some simp rules
|
file |
diff |
annotate
|
| Sat, 10 Jan 2009 01:06:32 +0100 |
wenzelm |
fixed proof involving dvd;
|
file |
diff |
annotate
|
| Fri, 19 Dec 2008 11:09:09 +0100 |
ballarin |
More porting to new locales
|
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
|
| Tue, 07 Oct 2008 16:07:50 +0200 |
haftmann |
arbitrary is undefined
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 17:31:20 +0200 |
ballarin |
Interpretation commands no longer accept interpretation attributes.
|
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, 15 Jan 2008 16:19:23 +0100 |
haftmann |
joined theories IntDef, Numeral, IntArith to theory Int
|
file |
diff |
annotate
|
| Thu, 02 Aug 2007 18:13:42 +0200 |
ballarin |
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
|
file |
diff |
annotate
|
| Tue, 24 Jul 2007 15:29:57 +0200 |
ballarin |
Interpretation of rings (as integers) maps defined operations to defined
|
file |
diff |
annotate
|
| Fri, 12 Jan 2007 15:37:21 +0100 |
ballarin |
Reverted to structure representation with records.
|
file |
diff |
annotate
|
| Fri, 22 Dec 2006 14:03:30 +0100 |
ballarin |
Experimenting with interpretations of "definition".
|
file |
diff |
annotate
|
| Mon, 16 Oct 2006 10:27:54 +0200 |
ballarin |
Order and lattice structures no longer based on records.
|
file |
diff |
annotate
|
| Thu, 03 Aug 2006 14:57:26 +0200 |
ballarin |
Restructured algebra library, added ideals and quotient rings.
|
file |
diff |
annotate
|