| Sat, 16 Sep 2023 06:38:44 +0000 |
haftmann |
reduced prominence of lemma names
|
file |
diff |
annotate
|
| Tue, 04 Jul 2023 12:53:01 +0100 |
paulson |
Another tranche of HOL Light material on metric and topological spaces
|
file |
diff |
annotate
|
| Sun, 07 May 2023 14:52:53 +0100 |
paulson |
Importation of additional lemmas from metric.ml
|
file |
diff |
annotate
|
| Tue, 02 May 2023 12:51:05 +0100 |
paulson |
A few new theorems
|
file |
diff |
annotate
|
| Thu, 02 Mar 2023 17:17:18 +0000 |
paulson |
Some new lemmas. Some tidying up
|
file |
diff |
annotate
|
| Sun, 14 Aug 2022 23:51:47 +0100 |
paulson |
moved some material from Sum_of_Powers
|
file |
diff |
annotate
|
| Wed, 08 Jun 2022 15:36:27 +0100 |
paulson |
some additional lemmas and a little tidying up
|
file |
diff |
annotate
|
| Thu, 24 Mar 2022 18:28:44 +0000 |
paulson |
Moving Dedekind_Real to the AFP
|
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
|
| Sun, 15 Nov 2020 07:17:06 +0000 |
haftmann |
bundles for reflected term syntax
|
file |
diff |
annotate
|
| Thu, 12 Nov 2020 09:06:44 +0100 |
haftmann |
bundled syntax for state monad combinators
|
file |
diff |
annotate
|
| Wed, 11 Nov 2020 14:27:17 +0000 |
paulson |
mult_le_cancel_iff1, mult_le_cancel_iff2, mult_less_iff1 generalised from the real_ versions
|
file |
diff |
annotate
|
| Mon, 12 Oct 2020 18:59:44 +0200 |
Mathias Fleury |
add reconstruction for the SMT solver veriT
|
file |
diff |
annotate
|
| Tue, 05 Nov 2019 19:55:42 +0100 |
nipkow |
moved duplicate lemmas up the hierarchy
|
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 07:18:55 +0000 |
haftmann |
streamlined setup for linear algebra, particularly removed redundant rule declarations
|
file |
diff |
annotate
|
| Wed, 15 May 2019 12:47:15 +0100 |
paulson |
Generalisations involving numerals; comparisons should now work for ennreal
|
file |
diff |
annotate
|
| Sun, 06 Jan 2019 15:04:34 +0100 |
wenzelm |
isabelle update -u path_cartouches;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sun, 23 Dec 2018 20:51:23 +0000 |
haftmann |
more rules
|
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
|
| Sat, 21 Jul 2018 13:30:43 +0200 |
paulson |
de-applying and removing junk
|
file |
diff |
annotate
|
| Thu, 19 Jul 2018 17:27:44 +0200 |
paulson |
de-applying
|
file |
diff |
annotate
|
| Thu, 28 Jun 2018 17:14:52 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Thu, 28 Jun 2018 14:13:57 +0100 |
paulson |
Generalising and renaming some basic results
|
file |
diff |
annotate
|
| Fri, 22 Jun 2018 20:31:49 +0200 |
wenzelm |
clarified document antiquotation @{theory};
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Tue, 19 Dec 2017 13:58:12 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Sat, 11 Nov 2017 18:41:08 +0000 |
haftmann |
dedicated definition for coprimality
|
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
|
| Mon, 09 Oct 2017 15:34:23 +0100 |
paulson |
new material about connectedness, etc.
|
file |
diff |
annotate
|
| Sat, 26 Aug 2017 16:47:25 +0200 |
nipkow |
reorganized and added log-related lemmas
|
file |
diff |
annotate
|
| Tue, 20 Jun 2017 21:41:59 +0200 |
haftmann |
stripped code pre/postprocessor setup for real from superfluous rules
|
file |
diff |
annotate
|
| Sun, 21 May 2017 21:37:31 +0200 |
blanchet |
added one more simplification to help replay
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
| Thu, 29 Sep 2016 20:54:45 +0200 |
boehmes |
invoke argo as part of the tried automatic proof methods
|
file |
diff |
annotate
|
| Thu, 29 Sep 2016 20:54:44 +0200 |
boehmes |
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
|
file |
diff |
annotate
|
| Fri, 12 Aug 2016 17:53:55 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Fri, 05 Aug 2016 16:22:13 +0200 |
nipkow |
added missing lemmas
|
file |
diff |
annotate
|
| Fri, 05 Aug 2016 09:30:20 +0200 |
nipkow |
tuned floor lemmas
|
file |
diff |
annotate
|
| Fri, 15 Jul 2016 11:07:51 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Thu, 23 Jun 2016 23:08:37 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2016 09:44:16 +0200 |
hoelzl |
move Conditional_Complete_Lattices to Main
|
file |
diff |
annotate
|
| Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
| Wed, 16 Mar 2016 13:57:06 +0000 |
paulson |
Contractible sets. Also removal of obsolete theorems and refactoring
|
file |
diff |
annotate
|
| Tue, 15 Mar 2016 14:08:25 +0000 |
paulson |
rationalisation of theorem names esp about "real Archimedian" etc.
|
file |
diff |
annotate
|
| Wed, 24 Feb 2016 16:00:57 +0000 |
paulson |
Merge
|
file |
diff |
annotate
|
| Wed, 24 Feb 2016 15:51:01 +0000 |
paulson |
Substantial new material for multivariate analysis. Also removal of some duplicates.
|
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
|
| Wed, 17 Feb 2016 21:51:57 +0100 |
haftmann |
generalized some lemmas;
|
file |
diff |
annotate
|
| Wed, 06 Jan 2016 12:18:53 +0100 |
hoelzl |
add the proof of the central limit theorem
|
file |
diff |
annotate
|
| Wed, 06 Jan 2016 13:04:30 +0100 |
blanchet |
more complete setup for 'Rat' in Nitpick
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 01:26:34 +0100 |
wenzelm |
prefer symbols for "abs";
|
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, 17 Nov 2015 12:32:08 +0000 |
paulson |
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
|
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
|
| 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
|
| Wed, 30 Sep 2015 16:36:42 +0100 |
paulson |
real_of_nat_Suc is now a simprule
|
file |
diff |
annotate
|