| 2013-11-01 |
haftmann |
2013-11-01 |
more simplification rules on unary and binary minus
|
file | diff | annotate |
| 2013-06-15 |
haftmann |
2013-06-15 |
lifting for primitive definitions;
explicit conversions from and to lists of coefficients, used for generated code;
replaced recursion operator poly_rec by fold_coeffs, preferring function definitions for non-trivial recursions;
prefer pre-existing gcd operation for gcd
|
file | diff | annotate |
| 2012-10-19 |
webertj |
2012-10-19 |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file | diff | annotate |
| 2012-10-12 |
wenzelm |
2012-10-12 |
discontinued obsolete typedef (open) syntax;
|
file | diff | annotate |
| 2012-04-06 |
wenzelm |
2012-04-06 |
fixed document;
|
file | diff | annotate |
| 2012-04-03 |
huffman |
2012-04-03 |
modernized obsolete old-style theory name with proper new-style underscore
|
file | diff | annotate |
| 2012-03-25 |
huffman |
2012-03-25 |
merged fork with new numeral representation (see NEWS)
|
file | diff | annotate |
| 2012-03-18 |
haftmann |
2012-03-18 |
comments for uniformity
|
file | diff | annotate |
| 2011-12-29 |
haftmann |
2011-12-29 |
tuned declaration
|
file | diff | annotate |
| 2011-12-20 |
bulwahn |
2011-12-20 |
adding quickcheck generators in some HOL-Library theories
|
file | diff | annotate |
| 2011-11-30 |
wenzelm |
2011-11-30 |
prefer typedef without extra definition and alternative name;
tuned proofs;
|
file | diff | annotate |
| 2011-11-20 |
wenzelm |
2011-11-20 |
eliminated obsolete "standard";
|
file | diff | annotate |
| 2011-09-12 |
nipkow |
2011-09-12 |
new fastforce replacing fastsimp - less confusing name
|
file | diff | annotate |
| 2011-03-13 |
wenzelm |
2011-03-13 |
tuned headers;
|
file | diff | annotate |
| 2010-09-13 |
nipkow |
2010-09-13 |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file | diff | annotate |
| 2010-09-07 |
nipkow |
2010-09-07 |
expand_fun_eq -> ext_iff
expand_set_eq -> set_ext_iff
Naming in line now with multisets
|
file | diff | annotate |
| 2010-08-27 |
haftmann |
2010-08-27 |
renamed class/constant eq to equal; tuned some instantiations
|
file | diff | annotate |
| 2010-07-12 |
haftmann |
2010-07-12 |
avoid explicit mandatory prefix markers when prefixes are mandatory implicitly
|
file | diff | annotate |
| 2010-07-12 |
haftmann |
2010-07-12 |
dropped superfluous [code del]s
|
file | diff | annotate |
| 2010-04-26 |
haftmann |
2010-04-26 |
dropped group_simps, ring_simps, field_eq_simps
|
file | diff | annotate |
| 2010-02-05 |
haftmann |
2010-02-05 |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file | diff | annotate |
| 2010-01-28 |
haftmann |
2010-01-28 |
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
|
file | diff | annotate |
| 2010-01-10 |
berghofe |
2010-01-10 |
Adapted to changes in induct method.
|
file | diff | annotate |
| 2009-07-14 |
haftmann |
2009-07-14 |
code attributes use common underscore convention
|
file | diff | annotate |
| 2009-06-16 |
huffman |
2009-06-16 |
smult_dvd lemmas; polynomial gcd
|
file | diff | annotate |
| 2009-04-29 |
haftmann |
2009-04-29 |
farewell to class recpower
|
file | diff | annotate |
| 2009-04-22 |
haftmann |
2009-04-22 |
power operation defined generic
|
file | diff | annotate |
| 2009-04-16 |
haftmann |
2009-04-16 |
tightended specification of class semiring_div
|
file | diff | annotate |
| 2009-03-27 |
haftmann |
2009-03-27 |
normalized imports
|
file | diff | annotate |
| 2009-03-04 |
huffman |
2009-03-04 |
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
|
file | diff | annotate |
| 2009-02-27 |
huffman |
2009-02-27 |
make list-style polynomial syntax work when show_sorts is on
|
file | diff | annotate |
| 2009-02-23 |
huffman |
2009-02-23 |
add lemmas poly_{div,mod}_minus_{left,right}
|
file | diff | annotate |
| 2009-02-18 |
huffman |
2009-02-18 |
move Polynomial.thy to Library
|
file | diff | annotate | base |