| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Wed, 08 Jul 2015 20:19:12 +0200 |
haftmann |
tuned facts
|
file |
diff |
annotate
|
| Thu, 25 Jun 2015 15:01:42 +0200 |
haftmann |
more theorems
|
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
|
| Tue, 31 Mar 2015 21:54:32 +0200 |
haftmann |
given up separate type classes demanding `inverse 0 = 0`
|
file |
diff |
annotate
|
| Mon, 23 Mar 2015 15:08:02 +0100 |
hoelzl |
fix parameter order of NO_MATCH
|
file |
diff |
annotate
|
| Tue, 10 Mar 2015 15:20:40 +0000 |
paulson |
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
|
file |
diff |
annotate
|
| Thu, 19 Feb 2015 11:53:36 +0100 |
haftmann |
establish unique preferred fact names
|
file |
diff |
annotate
|
| Sun, 15 Feb 2015 17:01:22 +0100 |
haftmann |
times_divide_eq rules are already [simp] despite of comment
|
file |
diff |
annotate
|
| Sat, 14 Feb 2015 10:24:15 +0100 |
haftmann |
less warnings
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Wed, 29 Oct 2014 19:01:49 +0100 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
| Fri, 24 Oct 2014 15:07:51 +0200 |
hoelzl |
use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
|
file |
diff |
annotate
|
| Thu, 02 Oct 2014 11:33:06 +0200 |
haftmann |
moved lemmas out of Int.thy which have nothing to do with int
|
file |
diff |
annotate
|
| Sat, 16 Aug 2014 14:12:39 +0200 |
wenzelm |
updated to named_theorems;
|
file |
diff |
annotate
|
| Sat, 05 Jul 2014 11:01:53 +0200 |
haftmann |
prefer ac_simps collections over separate name bindings for add and mult
|
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
|
| Mon, 14 Apr 2014 13:08:17 +0200 |
hoelzl |
added divide_nonneg_nonneg and co; made it a simp rule
|
file |
diff |
annotate
|
| Fri, 11 Apr 2014 22:53:33 +0200 |
nipkow |
made divide_pos_pos a simp rule
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 09:37:49 +0200 |
hoelzl |
add divide_simps
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 09:37:48 +0200 |
hoelzl |
field_simps: better support for negation and division, and power
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 09:37:47 +0200 |
hoelzl |
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
|
file |
diff |
annotate
|
| Sun, 06 Apr 2014 21:01:33 +0200 |
nipkow |
tuned lemmas: more general class
|
file |
diff |
annotate
|
| Sun, 06 Apr 2014 17:18:57 +0200 |
nipkow |
made field_simps "more complete"
|
file |
diff |
annotate
|
| Sat, 05 Apr 2014 01:04:46 +0100 |
paulson |
A single [simp] to handle the case -a/-b.
|
file |
diff |
annotate
|
| Fri, 04 Apr 2014 17:58:25 +0100 |
paulson |
divide_minus_left divide_minus_right are in field_simps but are not default simprules
|
file |
diff |
annotate
|
| Thu, 03 Apr 2014 23:51:52 +0100 |
paulson |
removing simprule status for divide_minus_left and divide_minus_right
|
file |
diff |
annotate
|
| Wed, 02 Apr 2014 16:34:37 +0100 |
paulson |
New theorems for extracting quotients
|
file |
diff |
annotate
|
| Mon, 24 Feb 2014 15:45:55 +0000 |
paulson |
A few lemmas about summations, etc.
|
file |
diff |
annotate
|