| Fri, 30 Aug 2024 10:16:48 +0100 |
paulson |
More tidying of old proofs
|
file |
diff |
annotate
|
| Fri, 09 Aug 2024 20:45:31 +0100 |
paulson |
revised/generalised some lemmas
|
file |
diff |
annotate
|
| Thu, 27 Jun 2024 16:52:17 +0000 |
haftmann |
dropped dubious dest rule which always unfolds a definition in the assumptions
|
file |
diff |
annotate
|
| Wed, 31 Jan 2024 21:10:52 +0100 |
wenzelm |
tuned proof: avoid z3;
|
file |
diff |
annotate
|
| Wed, 28 Dec 2022 12:15:16 +0000 |
paulson |
Tidied some messy proofs
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 08:42:36 +0200 |
desharna |
added opaque_combs and renamed hide_lams to opaque_lifting
|
file |
diff |
annotate
|
| Mon, 10 May 2021 16:14:34 +0200 |
wenzelm |
tuned proofs --- avoid z3, which is absent on arm64-linux;
|
file |
diff |
annotate
|
| Sun, 15 Nov 2020 07:17:06 +0000 |
haftmann |
bundles for reflected term syntax
|
file |
diff |
annotate
|
| Sun, 03 Nov 2019 19:58:02 -0500 |
immler |
moved theory Interval_Approximation from the AFP
|
file |
diff |
annotate
|
| Wed, 09 Oct 2019 14:51:54 +0000 |
haftmann |
dedicated fact collections for algebraic simplification rules potentially splitting goals
|
file |
diff |
annotate
|
| Sat, 22 Jun 2019 06:25:34 +0000 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Fri, 14 Jun 2019 08:34:28 +0000 |
haftmann |
official fact collection sign_simps
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 14:30:09 +0200 |
nipkow |
Prefix form of infix with * on either side no longer needs special treatment
|
file |
diff |
annotate
|
| Thu, 07 Jun 2018 19:36:12 +0200 |
nipkow |
utilize 'flip'
|
file |
diff |
annotate
|
| Mon, 05 Feb 2018 08:30:19 +0100 |
immler |
added lemmas, avoid 'float_of 0'
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| 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
|