| Sat, 02 Dec 2017 16:50:53 +0000 |
haftmann |
more simplification rules
|
file |
diff |
annotate
|
| Tue, 24 Oct 2017 18:48:21 +0200 |
immler |
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
|
file |
diff |
annotate
|
| Wed, 26 Apr 2017 15:53:35 +0100 |
paulson |
Further new material. The simprule status of some exp and ln identities was reverted.
|
file |
diff |
annotate
|
| Sun, 05 Mar 2017 10:57:51 +0100 |
nipkow |
added numeral_powr_numeral
|
file |
diff |
annotate
|
| Sun, 16 Oct 2016 09:31:06 +0200 |
haftmann |
eliminated irregular aliasses
|
file |
diff |
annotate
|
| Sun, 16 Oct 2016 09:31:04 +0200 |
haftmann |
more standardized names
|
file |
diff |
annotate
|
| Fri, 12 Aug 2016 09:57:09 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Fri, 12 Aug 2016 08:20:17 +0200 |
nipkow |
Extracted floorlog and bitlen to separate theory Log_Nat
|
file |
diff |
annotate
|
| Fri, 05 Aug 2016 12:27:51 +0200 |
nipkow |
fixed floor proofs
|
file |
diff |
annotate
|
| Fri, 05 Aug 2016 09:05:03 +0200 |
nipkow |
more lemmas
|
file |
diff |
annotate
|
| Fri, 24 Jun 2016 20:27:57 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Wed, 08 Jun 2016 16:46:48 +0200 |
immler |
generalized bitlen to floor of log
|
file |
diff |
annotate
|
| Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
| Fri, 26 Feb 2016 11:53:45 +0100 |
immler |
finite precision computation to determine sign for comparison
|
file |
diff |
annotate
|
| Fri, 26 Feb 2016 11:53:45 +0100 |
immler |
positive precision for truncate; fixed precision for approximation of rationals; code for truncate
|
file |
diff |
annotate
|
| Fri, 26 Feb 2016 11:53:42 +0100 |
immler |
compute_real_of_float has not been used as code equation
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:57 +0100 |
haftmann |
dropped various legacy fact bindings
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 01:28:28 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Sun, 27 Dec 2015 21:46:36 +0100 |
wenzelm |
prefer symbols for "floor", "ceiling";
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Tue, 01 Dec 2015 14:09:10 +0000 |
paulson |
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
|
file |
diff |
annotate
|
| Fri, 13 Nov 2015 12:27:13 +0000 |
paulson |
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
|
file |
diff |
annotate
|
| Wed, 11 Nov 2015 17:11:50 +0000 |
paulson |
new conversion theorems for int, nat to float
|
file |
diff |
annotate
|
| Tue, 10 Nov 2015 14:18:41 +0000 |
paulson |
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
|
file |
diff |
annotate
|
| Sat, 08 Aug 2015 10:51:33 +0200 |
haftmann |
direct bootstrap of integer division from natural division
|
file |
diff |
annotate
|
| Thu, 09 Jul 2015 00:40:57 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2015 22:57:34 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 17 Jun 2015 11:03:05 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Sun, 07 Jun 2015 14:36:36 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|