| #
8c6db6b8 |
|
26-Jun-2018 |
paulson <lp15@cam.ac.uk> |
a few new lemmas
|
| #
a50a819c |
|
17-Jun-2018 |
paulson <lp15@cam.ac.uk> |
Algebra tidy-up
|
| #
457595a5 |
|
14-Jun-2018 |
paulson <lp15@cam.ac.uk> |
Adjusting Number_Theory for new Algebra
|
| #
17e1fb25 |
|
14-Jun-2018 |
paulson <lp15@cam.ac.uk> |
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
|
| #
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
| #
94df9708 |
|
05-Jan-2018 |
nipkow <none@none> |
Renamed (^) to [^] in preparation of the move from "op X" to (X)
|
| #
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
| #
66281660 |
|
26-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
72a7ccdd |
|
08-Jan-2016 |
wenzelm <none@none> |
tuned;
|
| #
6c667f5f |
|
10-Oct-2015 |
wenzelm <none@none> |
prefer symbols;
|
| #
2c29a4b9 |
|
10-Oct-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
f55b23fd |
|
23-Jul-2015 |
wenzelm <none@none> |
more symbols by default, without xsymbols mode;
|
| #
a1fd7718 |
|
17-Apr-2015 |
Rene Thiemann <rene.thiemann@uibk.ac.at> |
finprod takes 1 in case of infinite sets => remove several "finite A" assumptions
|
| #
0551f7de |
|
01-Nov-2014 |
wenzelm <none@none> |
eliminated spurious semicolons;
|
| #
57bf4f8e |
|
14-Mar-2014 |
wenzelm <none@none> |
tuned -- command 'text' was localized some years ago;
|
| #
cbddf8f8 |
|
27-Feb-2012 |
wenzelm <none@none> |
tuned proofs;
|
| #
ad9e459c |
|
11-Sep-2011 |
nipkow <none@none> |
new fastforce replacing fastsimp - less confusing name
|
| #
47ae4aab |
|
06-Jan-2011 |
ballarin <none@none> |
Abelian group facts obtained from group facts via interpretation (sublocale).
|
| #
9e4cf179 |
|
28-Nov-2010 |
nipkow <none@none> |
gave more standard finite set rules simp and intro attribute
|
| #
7d4dd605 |
|
21-Mar-2010 |
wenzelm <none@none> |
standard headers;
|
| #
40c700e0 |
|
21-Mar-2010 |
wenzelm <none@none> |
slightly more uniform definitions -- eliminated old-style meta-equality;
|
| #
84c0e788 |
|
21-Mar-2010 |
wenzelm <none@none> |
eliminated old constdefs;
|
| #
baea5702 |
|
01-Mar-2010 |
haftmann <none@none> |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
| #
3403212c |
|
08-Feb-2010 |
wenzelm <none@none> |
modernized some syntax translations;
|
| #
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
|
| #
f9ce79eb |
|
21-Sep-2009 |
haftmann <none@none> |
tuned proofs
|
| #
99760ce7 |
|
19-Jun-2009 |
nipkow <none@none> |
Made Pi_I [simp]
|
| #
290d2fc3 |
|
16-Dec-2008 |
ballarin <none@none> |
More porting to new locales.
|
| #
16362266 |
|
07-Oct-2008 |
haftmann <none@none> |
arbitrary is undefined
|
| #
0352bc4b |
|
18-Aug-2008 |
ballarin <none@none> |
Theorem on polynomial division and lemmas.
|
| #
fa753c2e |
|
01-Aug-2008 |
ballarin <none@none> |
Generalised polynomial lemmas from cring to ring.
|
| #
52a09abc |
|
29-Jul-2008 |
ballarin <none@none> |
New theorems on summation.
|
| #
7b63d2a6 |
|
11-Jul-2007 |
berghofe <none@none> |
Adapted to new inductive definition package.
|
| #
666949b2 |
|
12-Jun-2007 |
wenzelm <none@none> |
tuned proofs: avoid implicit prems;
|
| #
95ffe831 |
|
07-Feb-2007 |
berghofe <none@none> |
Adapted to changes in Finite_Set theory.
|
| #
9cb553a1 |
|
03-Aug-2006 |
ballarin <none@none> |
Restructured algebra library, added ideals and quotient rings.
|
| #
6ad72692 |
|
01-Jul-2005 |
berghofe <none@none> |
Removed setsubgoaler hack.
|
| #
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
| #
058ecede |
|
24-Nov-2004 |
nipkow <none@none> |
mod because of change in finite set induction
|
| #
ad18463f |
|
02-Aug-2004 |
ballarin <none@none> |
Theories now take advantage of recent syntax improvements with (structure).
|
| #
75db8328 |
|
14-May-2004 |
paulson <none@none> |
tidied
|
| #
840009b7 |
|
06-May-2004 |
wenzelm <none@none> |
tuned document;
|
| #
7e80ef11 |
|
23-Apr-2004 |
wenzelm <none@none> |
improved notation;
|
| #
649e8e50 |
|
22-Apr-2004 |
wenzelm <none@none> |
improved notation;
|
| #
b94d2850 |
|
16-Apr-2004 |
wenzelm <none@none> |
simplified ML code for setsubgoaler;
|
| #
cd8e19bf |
|
30-Sep-2003 |
ballarin <none@none> |
Changed order of prems in finprod_cong. Slight speedup.
|
| #
e6fe55e4 |
|
30-Apr-2003 |
ballarin <none@none> |
Greatly extended CRing. Added Module.
|