| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
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
|
| Mon, 01 Jun 2015 18:59:20 +0200 |
haftmann |
correct sort constraints for abbreviations in type classes
|
file |
diff |
annotate
|
| Mon, 23 Mar 2015 19:05:14 +0100 |
haftmann |
distributivity of partial minus establishes desired properties of dvd in semirings
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Sun, 26 Oct 2014 19:11:16 +0100 |
haftmann |
eliminated redundancies;
|
file |
diff |
annotate
|
| Thu, 23 Oct 2014 19:40:41 +0200 |
haftmann |
even further downshift of theory Parity in the hierarchy
|
file |
diff |
annotate
|
| Thu, 23 Oct 2014 19:40:39 +0200 |
haftmann |
further downshift of theory Parity in the hierarchy
|
file |
diff |
annotate
|
| Thu, 23 Oct 2014 14:04:05 +0200 |
haftmann |
slight generalization and unification of simp rules for algebraic procedures
|
file |
diff |
annotate
|
| Thu, 23 Oct 2014 14:04:05 +0200 |
haftmann |
downshift of theory Parity in the hierarchy
|
file |
diff |
annotate
|
| Thu, 23 Oct 2014 14:04:05 +0200 |
haftmann |
parity induction over natural numbers
|
file |
diff |
annotate
|
| Tue, 21 Oct 2014 21:10:44 +0200 |
haftmann |
turn even into an abbreviation
|
file |
diff |
annotate
|
| Mon, 20 Oct 2014 17:00:13 +0200 |
wenzelm |
repared document;
|
file |
diff |
annotate
|
| Mon, 20 Oct 2014 07:57:33 +0200 |
haftmann |
more standard declaration for presburger
|
file |
diff |
annotate
|
| Mon, 20 Oct 2014 07:45:58 +0200 |
haftmann |
augmented and tuned facts on even/odd and division
|
file |
diff |
annotate
|
| Sun, 19 Oct 2014 18:05:26 +0200 |
haftmann |
prefer generic elimination rules for even/odd over specialized unfold rules for nat
|
file |
diff |
annotate
|
| Thu, 16 Oct 2014 19:26:28 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 16 Oct 2014 19:26:27 +0200 |
haftmann |
standard elimination rule for even
|
file |
diff |
annotate
|
| Thu, 16 Oct 2014 19:26:26 +0200 |
haftmann |
tuned facts on even and power
|
file |
diff |
annotate
|
| Thu, 16 Oct 2014 19:26:14 +0200 |
haftmann |
restructured
|
file |
diff |
annotate
|
| Thu, 16 Oct 2014 19:26:13 +0200 |
haftmann |
even more cleanup
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 08:23:23 +0200 |
haftmann |
legacy cleanup
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 08:23:23 +0200 |
haftmann |
more algebraic deductions for facts on even/odd
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 08:23:23 +0200 |
haftmann |
more algebraic deductions for facts on even/odd
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 08:23:23 +0200 |
haftmann |
purely algebraic characterization of even and odd
|
file |
diff |
annotate
|
| Thu, 09 Oct 2014 22:43:48 +0200 |
haftmann |
more foundational definition for predicate even
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Thu, 31 Oct 2013 11:44:20 +0100 |
haftmann |
purely algebraic foundation for even/odd
|
file |
diff |
annotate
|
| Thu, 31 Oct 2013 11:44:20 +0100 |
haftmann |
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 15:43:30 +0200 |
huffman |
remove redundant simp rule
|
file |
diff |
annotate
|