| Thu, 06 Aug 2015 23:56:48 +0200 |
haftmann |
slight cleanup of lemmas
|
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
|
| Fri, 19 Jun 2015 07:53:33 +0200 |
haftmann |
generalized some theorems about integral domains and moved to HOL theories
|
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:22 +0200 |
haftmann |
implicit partial divison operation in integral domains
|
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:16 +0200 |
hoelzl |
replace Filters in NSA by HOL-Filters
|
file |
diff |
annotate
|
| Sun, 12 Apr 2015 11:33:19 +0200 |
hoelzl |
move filters to their own theory
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 21:54:32 +0200 |
haftmann |
given up separate type classes demanding `inverse 0 = 0`
|
file |
diff |
annotate
|
| Sat, 28 Mar 2015 21:32:48 +0100 |
haftmann |
clarified no_zero_devisors: makes only sense in a semiring;
|
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
|
| Mon, 23 Mar 2015 19:05:14 +0100 |
haftmann |
explicit commutative additive inverse operation;
|
file |
diff |
annotate
|
| Thu, 12 Mar 2015 14:08:47 +0100 |
Andreas Lochbihler |
make proofs work with 4762c690a75c
|
file |
diff |
annotate
|
| Tue, 10 Mar 2015 16:35:14 +0100 |
Andreas Lochbihler |
more type class instances
|
file |
diff |
annotate
|
| Thu, 19 Feb 2015 11:53:36 +0100 |
haftmann |
establish unique preferred fact names
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:13:28 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Wed, 29 Oct 2014 17:01:44 +0100 |
wenzelm |
modernized setup;
|
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
|
| Sat, 22 Mar 2014 20:42:16 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Tue, 04 Mar 2014 15:26:12 -0800 |
huffman |
remove simp rules made redundant by the replacement of neg_numeral with negated numerals
|
file |
diff |
annotate
|
| Mon, 25 Nov 2013 12:27:03 +0100 |
traytel |
adapt to 9733ab5c1df6
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 18:58:20 +0200 |
wenzelm |
discontinued obsolete typedef (open) syntax;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Thu, 12 Apr 2012 18:39:19 +0200 |
wenzelm |
more standard method setup;
|
file |
diff |
annotate
|
| Wed, 04 Apr 2012 09:00:10 +0200 |
huffman |
rename ML structure to avoid shadowing earlier name
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Wed, 28 Dec 2011 20:03:13 +0100 |
wenzelm |
reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
|
file |
diff |
annotate
|