Wed, 25 May 2016 11:49:40 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
Tue, 26 Apr 2016 22:44:31 +0200 |
wenzelm |
some uses of 'obtain' with structure statement;
|
file |
diff |
annotate
|
Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
Wed, 20 Apr 2016 16:50:20 +0200 |
Rene Thiemann |
fixed code equation for pdivmod, added improved code equation for pseudo_mod
|
file |
diff |
annotate
|
Wed, 20 Apr 2016 16:01:59 +0200 |
wenzelm |
proper latex;
|
file |
diff |
annotate
|
Fri, 15 Apr 2016 10:19:35 +0200 |
Rene Thiemann |
several updates on polynomial long division and pseudo division
|
file |
diff |
annotate
|
Thu, 25 Feb 2016 16:44:53 +0100 |
eberlm |
Tuned Euclidean rings
|
file |
diff |
annotate
|
Wed, 17 Feb 2016 21:51:58 +0100 |
haftmann |
separated potentially conflicting type class instance into separate theory
|
file |
diff |
annotate
|
Wed, 17 Feb 2016 21:51:58 +0100 |
haftmann |
gcd instances for poly
|
file |
diff |
annotate
|
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
|
Tue, 05 Jan 2016 21:57:21 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
Tue, 05 Jan 2016 20:23:49 +0100 |
eberlm |
Fixed sectioning in HOL/Library/Polynomial
|
file |
diff |
annotate
|
Tue, 05 Jan 2016 17:54:10 +0100 |
eberlm |
Added some facts about polynomials
|
file |
diff |
annotate
|
Mon, 28 Dec 2015 01:28:28 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
Mon, 09 Nov 2015 15:48:17 +0100 |
wenzelm |
qualifier is mandatory by default;
|
file |
diff |
annotate
|
Thu, 05 Nov 2015 10:39:49 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
Thu, 24 Sep 2015 13:33:42 +0200 |
wenzelm |
explicit indication of overloaded typedefs;
|
file |
diff |
annotate
|
Wed, 08 Jul 2015 14:01:39 +0200 |
haftmann |
more algebraic properties for gcd/lcm
|
file |
diff |
annotate
|
Wed, 08 Jul 2015 14:01:34 +0200 |
haftmann |
moved normalization and unit_factor into Main HOL corpus
|
file |
diff |
annotate
|
Mon, 06 Jul 2015 22:57:34 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Thu, 25 Jun 2015 15:01:42 +0200 |
haftmann |
more theorems
|
file |
diff |
annotate
|
Tue, 23 Jun 2015 16:55:28 +0100 |
paulson |
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
|
file |
diff |
annotate
|
Wed, 17 Jun 2015 11:03:05 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
Fri, 12 Jun 2015 08:53:23 +0200 |
haftmann |
uniform _ div _ as infix syntax for ring division
|
file |
diff |
annotate
|
Mon, 01 Jun 2015 18:59:21 +0200 |
haftmann |
separate class for division operator, with particular syntax added in more specific classes
|
file |
diff |
annotate
|
Sun, 12 Apr 2015 11:34:09 +0200 |
hoelzl |
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
|
file |
diff |
annotate
|
Thu, 09 Apr 2015 15:17:21 +0200 |
hoelzl |
replace almost_everywhere_zero by Infinite_Set.MOST
|
file |
diff |
annotate
|
Mon, 23 Mar 2015 19:05:14 +0100 |
haftmann |
explicit commutative additive inverse operation;
|
file |
diff |
annotate
|
Thu, 19 Feb 2015 11:53:36 +0100 |
haftmann |
establish unique preferred fact names
|
file |
diff |
annotate
|
Fri, 06 Feb 2015 17:57:03 +0100 |
haftmann |
default abstypes and default abstract equations make technical (no_code) annotation superfluous
|
file |
diff |
annotate
|