| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
| 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
|
| Wed, 30 Nov 2011 16:27:10 +0100 |
wenzelm |
prefer typedef without extra definition and alternative name;
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 21:05:23 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Thu, 17 Nov 2011 08:07:54 +0100 |
huffman |
HOL-NSA: add number_semiring instance, reformulate several lemmas using '2' instead of '1+1'
|
file |
diff |
annotate
|
| Mon, 29 Nov 2010 13:44:54 +0100 |
haftmann |
equivI has replaced equiv.intro
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 11:17:13 +0200 |
haftmann |
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
|
file |
diff |
annotate
|
| Fri, 20 Aug 2010 17:46:56 +0200 |
haftmann |
more concise characterization of of_nat operation and class semiring_char_0
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 08:58:13 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 09:49:36 +0200 |
haftmann |
tuned class linordered_field_inverse_zero
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 08:17:40 +0200 |
haftmann |
instances for *_inverse_zero classes
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 11:34:17 +0200 |
haftmann |
class division_ring_inverse_zero
|
file |
diff |
annotate
|
| Wed, 10 Feb 2010 08:49:26 +0100 |
haftmann |
division ring assumes divide_inverse
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 17:12:38 +0100 |
haftmann |
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 14:22:22 +0100 |
haftmann |
dropped accidental duplication of "lin" prefix from cs. 108662d50512
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 14:06:48 +0100 |
haftmann |
dropped instantiations for combined lattices
|
file |
diff |
annotate
|
| Fri, 05 Feb 2010 14:33:50 +0100 |
haftmann |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file |
diff |
annotate
|
| Wed, 29 Apr 2009 14:20:26 +0200 |
haftmann |
farewell to class recpower
|
file |
diff |
annotate
|
| Thu, 23 Apr 2009 12:17:51 +0200 |
haftmann |
adaptions due to rearrangment of power operation
|
file |
diff |
annotate
|
| Thu, 26 Mar 2009 20:08:55 +0100 |
wenzelm |
interpretation/interpret: prefixes are mandatory by default;
|
file |
diff |
annotate
|
| Mon, 02 Mar 2009 16:53:55 +0100 |
nipkow |
name changes
|
file |
diff |
annotate
|
| Fri, 13 Feb 2009 14:12:00 -0800 |
huffman |
add class cancel_comm_monoid_add
|
file |
diff |
annotate
|
| Mon, 15 Dec 2008 18:12:52 +0100 |
ballarin |
More porting to new locales.
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Fri, 29 Aug 2008 08:14:58 +0200 |
haftmann |
fixed names of class assumptions
|
file |
diff |
annotate
|
| Fri, 25 Jul 2008 12:03:34 +0200 |
haftmann |
added class preorder
|
file |
diff |
annotate
|
| Fri, 18 Jul 2008 18:25:53 +0200 |
haftmann |
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
|
file |
diff |
annotate
|
| Thu, 03 Jul 2008 17:47:22 +0200 |
huffman |
move nonstandard analysis theories to NSA directory
|
file |
diff |
annotate
|