| Mon, 11 Jan 2016 16:38:39 +0100 |
eberlm |
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 01:28:28 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Thu, 05 Nov 2015 10:39:49 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Wed, 24 Jun 2015 23:03:55 +0200 |
wenzelm |
tuned proofs -- less digits;
|
file |
diff |
annotate
|
| Mon, 22 Jun 2015 21:07:10 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 13 Jun 2015 19:53:53 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 13 Jun 2015 13:09:05 +0200 |
wenzelm |
renamed "prems" to "that";
|
file |
diff |
annotate
|
| Wed, 10 Jun 2015 23:34:23 +0200 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Thu, 19 Feb 2015 11:53:36 +0100 |
haftmann |
establish unique preferred fact names
|
file |
diff |
annotate
|
| Wed, 18 Feb 2015 22:46:48 +0100 |
haftmann |
eliminated fact duplicates
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:20:45 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Tue, 05 Aug 2014 12:56:15 +0200 |
wenzelm |
tuned proofs;
|
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 12:25:35 +0200 |
hoelzl |
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
|
file |
diff |
annotate
|
| Tue, 29 Apr 2014 21:54:26 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Mon, 28 Apr 2014 23:43:13 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Mon, 28 Apr 2014 17:48:59 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 12 Apr 2014 17:26:27 +0200 |
nipkow |
made mult_pos_pos a simp rule
|
file |
diff |
annotate
|
| Fri, 04 Apr 2014 14:44:51 +0200 |
blanchet |
tuned spaces
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 17:06:17 +0000 |
paulson |
generalised some results using type classes
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 16:17:20 +0000 |
paulson |
More complex-related lemmas
|
file |
diff |
annotate
|
| Fri, 07 Feb 2014 17:43:47 +0000 |
paulson |
Simplified some proofs, deleting a lot of strange unused material at the end of the theory.
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 09:45:02 +0100 |
hoelzl |
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
|
file |
diff |
annotate
|
| Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
| Sun, 18 Aug 2013 19:59:19 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Sat, 15 Jun 2013 17:19:23 +0200 |
haftmann |
lifting for primitive definitions;
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 19:43:31 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 14:14:39 +0100 |
wenzelm |
more standard imports;
|
file |
diff |
annotate
|
| Sun, 30 Dec 2012 16:23:30 +0100 |
wenzelm |
uniform notation for == and \<equiv> (cf. 3e3c2af5e8a5);
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
| Tue, 17 Jan 2012 16:30:54 +0100 |
huffman |
factor-cancellation simprocs now call the full simplifier to prove that factors are non-zero
|
file |
diff |
annotate
|
| Wed, 12 Jan 2011 17:19:50 +0100 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
| Mon, 19 Jul 2010 16:09:44 +0200 |
haftmann |
diff_minus subsumes diff_def
|
file |
diff |
annotate
|
| Sun, 23 May 2010 17:22:30 +0100 |
webertj |
Typo fixed.
|
file |
diff |
annotate
|
| Mon, 17 May 2010 16:52:34 -0700 |
huffman |
simplify proof
|
file |
diff |
annotate
|
| Sun, 09 May 2010 22:51:11 -0700 |
huffman |
avoid using real-specific versions of generic lemmas
|
file |
diff |
annotate
|
| Sun, 10 Jan 2010 18:43:45 +0100 |
berghofe |
Adapted to changes in induct method.
|
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
|
| Thu, 28 May 2009 23:03:12 -0700 |
huffman |
LIMSEQ_def -> LIMSEQ_iff
|
file |
diff |
annotate
|
| Wed, 29 Apr 2009 14:20:26 +0200 |
haftmann |
farewell to class recpower
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 08:57:03 -0700 |
huffman |
remove trailing spaces
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Mon, 02 Mar 2009 12:33:12 +0000 |
chaieb |
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
|
file |
diff |
annotate
|
| Wed, 18 Feb 2009 09:47:58 -0800 |
huffman |
move polynomial order stuff from Fundamental_Theorem_Algebra to Polynomial
|
file |
diff |
annotate
|
| Thu, 12 Feb 2009 18:14:43 +0100 |
nipkow |
Moved FTA into Lib and cleaned it up a little.
|
file |
diff |
annotate
| base
|