| 2019-01-04 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| 2018-12-23 |
haftmann |
more rules
|
file |
diff |
annotate
|
| 2018-10-27 |
nipkow |
moved lemmas
|
file |
diff |
annotate
|
| 2018-06-06 |
wenzelm |
proper white space;
|
file |
diff |
annotate
|
| 2018-05-12 |
haftmann |
removed some non-essential rules
|
file |
diff |
annotate
|
| 2018-04-24 |
haftmann |
proper datatype for 8-bit characters
|
file |
diff |
annotate
|
| 2018-04-20 |
haftmann |
algebraic embeddings for bit operations
|
file |
diff |
annotate
|
| 2018-04-16 |
haftmann |
explicit simp rules for computing abstract bit operations
|
file |
diff |
annotate
|
| 2018-04-05 |
haftmann |
even more on bit operations
|
file |
diff |
annotate
|
| 2018-04-04 |
haftmann |
more bit operation conversions
|
file |
diff |
annotate
|
| 2018-03-21 |
haftmann |
tuned proof
|
file |
diff |
annotate
|
| 2018-03-21 |
haftmann |
prefer convention to place operation name before type name
|
file |
diff |
annotate
|
| 2018-03-20 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| 2018-03-20 |
haftmann |
generalized
|
file |
diff |
annotate
|
| 2018-03-12 |
haftmann |
eliminiated superfluous class semiring_bits
|
file |
diff |
annotate
|
| 2018-03-10 |
haftmann |
abstract algebraic bit operations
|
file |
diff |
annotate
|
| 2018-01-08 |
paulson |
moved in some material from Euler-MacLaurin
|
file |
diff |
annotate
|
| 2017-11-23 |
haftmann |
new simp rule
|
file |
diff |
annotate
|
| 2017-11-11 |
haftmann |
dedicated definition for coprimality
|
file |
diff |
annotate
|
| 2017-10-09 |
haftmann |
canonical multiplicative euclidean size
|
file |
diff |
annotate
|
| 2017-10-09 |
haftmann |
clarified parity
|
file |
diff |
annotate
|
| 2017-10-08 |
haftmann |
more fundamental definition of div and mod on int
|
file |
diff |
annotate
|
| 2017-10-08 |
haftmann |
one uniform type class for parity structures
|
file |
diff |
annotate
|
| 2017-10-08 |
haftmann |
elementary definition of division on natural numbers
|
file |
diff |
annotate
|
| 2017-08-27 |
bulwahn |
another fact on (- 1) ^ _
|
file |
diff |
annotate
|
| 2017-01-04 |
haftmann |
moved euclidean ring to HOL
|
file |
diff |
annotate
|
| 2016-08-10 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| 2016-03-12 |
haftmann |
model characters directly as range 0..255
|
file |
diff |
annotate
|
| 2016-01-06 |
hoelzl |
add the proof of the central limit theorem
|
file |
diff |
annotate
|
| 2015-12-07 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| 2015-11-02 |
eberlm |
Rounding function, uniform limits, cotangent, binomial identities
|
file |
diff |
annotate
|
| 2015-08-06 |
haftmann |
slight cleanup of lemmas
|
file |
diff |
annotate
|
| 2015-07-18 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| 2015-06-23 |
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
|
| 2015-06-01 |
haftmann |
correct sort constraints for abbreviations in type classes
|
file |
diff |
annotate
|
| 2015-03-23 |
haftmann |
distributivity of partial minus establishes desired properties of dvd in semirings
|
file |
diff |
annotate
|
| 2014-11-02 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| 2014-10-26 |
haftmann |
eliminated redundancies;
|
file |
diff |
annotate
|
| 2014-10-23 |
haftmann |
even further downshift of theory Parity in the hierarchy
|
file |
diff |
annotate
|
| 2014-10-23 |
haftmann |
further downshift of theory Parity in the hierarchy
|
file |
diff |
annotate
|
| 2014-10-23 |
haftmann |
slight generalization and unification of simp rules for algebraic procedures
|
file |
diff |
annotate
|
| 2014-10-23 |
haftmann |
downshift of theory Parity in the hierarchy
|
file |
diff |
annotate
|
| 2014-10-23 |
haftmann |
parity induction over natural numbers
|
file |
diff |
annotate
|
| 2014-10-21 |
haftmann |
turn even into an abbreviation
|
file |
diff |
annotate
|
| 2014-10-20 |
wenzelm |
repared document;
|
file |
diff |
annotate
|
| 2014-10-20 |
haftmann |
more standard declaration for presburger
|
file |
diff |
annotate
|
| 2014-10-20 |
haftmann |
augmented and tuned facts on even/odd and division
|
file |
diff |
annotate
|
| 2014-10-19 |
haftmann |
prefer generic elimination rules for even/odd over specialized unfold rules for nat
|
file |
diff |
annotate
|
| 2014-10-16 |
haftmann |
tuned
|
file |
diff |
annotate
|
| 2014-10-16 |
haftmann |
standard elimination rule for even
|
file |
diff |
annotate
|
| 2014-10-16 |
haftmann |
tuned facts on even and power
|
file |
diff |
annotate
|
| 2014-10-16 |
haftmann |
restructured
|
file |
diff |
annotate
|
| 2014-10-16 |
haftmann |
even more cleanup
|
file |
diff |
annotate
|
| 2014-10-14 |
haftmann |
legacy cleanup
|
file |
diff |
annotate
|
| 2014-10-14 |
haftmann |
more algebraic deductions for facts on even/odd
|
file |
diff |
annotate
|
| 2014-10-14 |
haftmann |
more algebraic deductions for facts on even/odd
|
file |
diff |
annotate
|
| 2014-10-14 |
haftmann |
purely algebraic characterization of even and odd
|
file |
diff |
annotate
|
| 2014-10-09 |
haftmann |
more foundational definition for predicate even
|
file |
diff |
annotate
|
| 2013-11-19 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| 2013-10-31 |
haftmann |
purely algebraic foundation for even/odd
|
file |
diff |
annotate
|