| Mon, 11 May 2020 11:15:41 +0100 |
paulson |
the Uniq quantifier
|
file |
diff |
annotate
|
| Sun, 05 Apr 2020 17:12:26 +0100 |
paulson |
Tidied up more ancient, horrible proofs. Liberalised frac_le
|
file |
diff |
annotate
|
| Sat, 14 Mar 2020 15:58:51 +0000 |
paulson |
tidied up a few little proofs
|
file |
diff |
annotate
|
| Wed, 17 Apr 2019 21:53:45 +0100 |
paulson |
moved subset_image_inj into Hilbert_Choice
|
file |
diff |
annotate
|
| Wed, 10 Apr 2019 13:34:55 +0100 |
paulson |
The last big tranche of Homology material: invariance of domain; renamings to use generic sum/prod lemmas from their locale
|
file |
diff |
annotate
|
| Thu, 14 Mar 2019 16:55:06 +0100 |
wenzelm |
more specific keyword kinds;
|
file |
diff |
annotate
|
| Tue, 05 Mar 2019 07:00:21 +0000 |
haftmann |
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
|
file |
diff |
annotate
|
| Thu, 31 Jan 2019 13:08:59 +0000 |
haftmann |
proper congruence rule for image operator
|
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
|
| Wed, 19 Dec 2018 08:16:42 +0000 |
haftmann |
tuned proof text
|
file |
diff |
annotate
|
| Wed, 19 Dec 2018 08:16:41 +0000 |
haftmann |
tuned proof
|
file |
diff |
annotate
|
| Sat, 10 Nov 2018 07:57:19 +0000 |
haftmann |
clarified status of legacy input abbreviations
|
file |
diff |
annotate
|
| Tue, 11 Sep 2018 16:21:54 +0100 |
paulson |
A few new results, elimination of duplicates and more use of "pairwise"
|
file |
diff |
annotate
|
| Fri, 24 Aug 2018 20:22:14 +0000 |
haftmann |
some modernization of notation
|
file |
diff |
annotate
|
| Wed, 11 Jul 2018 01:04:23 +0200 |
nipkow |
moved lemmas
|
file |
diff |
annotate
|
| Mon, 26 Mar 2018 16:14:16 +0200 |
Manuel Eberl |
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
|
file |
diff |
annotate
|
| Mon, 12 Mar 2018 20:52:53 +0100 |
Manuel Eberl |
Changes to complete distributive lattices due to Viorel Preoteasa
|
file |
diff |
annotate
|
| Mon, 19 Feb 2018 16:44:45 +0000 |
paulson |
lots of new material, ultimately related to measure theory
|
file |
diff |
annotate
|
| Thu, 15 Feb 2018 12:11:00 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Sun, 28 May 2017 15:46:26 +0200 |
nipkow |
removed GreatestM
|
file |
diff |
annotate
|
| Sun, 28 May 2017 13:57:43 +0200 |
nipkow |
introduced arg_max
|
file |
diff |
annotate
|
| Sun, 28 May 2017 08:07:40 +0200 |
nipkow |
removed LeastM; is now arg_min
|
file |
diff |
annotate
|
| Sun, 14 May 2017 12:46:32 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Sat, 17 Dec 2016 15:22:13 +0100 |
haftmann |
restructured matter on polynomials and normalized fractions
|
file |
diff |
annotate
|
| Sat, 01 Oct 2016 19:29:48 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 01 Oct 2016 17:38:14 +0200 |
wenzelm |
Isar proof of Schroeder_Bernstein without using Hilbert_Choice (and metis);
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 23:39:15 +0200 |
wenzelm |
clarified obscure facts;
|
file |
diff |
annotate
|
| Mon, 08 Aug 2016 19:34:00 +0200 |
wenzelm |
tuned proof;
|
file |
diff |
annotate
|
| Mon, 08 Aug 2016 18:55:12 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 05 Aug 2016 18:14:28 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Fri, 22 Jul 2016 11:00:43 +0200 |
wenzelm |
tuned proofs -- avoid unstructured calculation;
|
file |
diff |
annotate
|
| Mon, 04 Jul 2016 19:46:19 +0200 |
haftmann |
dedicated locale for total bijections
|
file |
diff |
annotate
|
| Sat, 02 Jul 2016 08:41:05 +0200 |
haftmann |
more theorems
|
file |
diff |
annotate
|
| Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
| Mon, 21 Mar 2016 21:18:08 +0100 |
wenzelm |
clarified rule structure;
|
file |
diff |
annotate
|
| Sat, 05 Mar 2016 19:58:56 +0100 |
wenzelm |
old HOL syntax is for input only;
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:56 +0100 |
haftmann |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
file |
diff |
annotate
|
| Sat, 19 Dec 2015 20:02:51 +0100 |
blanchet |
removed subsumed dependency
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
| Thu, 27 Aug 2015 21:19:48 +0200 |
haftmann |
standardized some occurences of ancient "split" alias
|
file |
diff |
annotate
|
| Wed, 19 Aug 2015 19:18:19 +0100 |
paulson |
New material and fixes related to the forthcoming Stone-Weierstrass development
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Fri, 26 Jun 2015 10:20:33 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Thu, 04 Dec 2014 16:51:54 +0100 |
haftmann |
cleaned up mess
|
file |
diff |
annotate
|
| Thu, 13 Nov 2014 17:19:52 +0100 |
hoelzl |
import general theorems from AFP/Markov_Models
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Mon, 29 Sep 2014 14:32:30 +0200 |
blanchet |
made 'moura' tactic more powerful
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 23:57:26 +0200 |
blanchet |
renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 16:58:27 +0200 |
blanchet |
moved skolem method
|
file |
diff |
annotate
|
| Mon, 30 Jun 2014 15:45:25 +0200 |
hoelzl |
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
|
file |
diff |
annotate
|
| Wed, 18 Jun 2014 07:31:12 +0200 |
hoelzl |
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
|
file |
diff |
annotate
|
| Sat, 26 Apr 2014 13:25:45 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Wed, 16 Apr 2014 21:51:41 +0200 |
haftmann |
more simp rules for Fun.swap
|
file |
diff |
annotate
|
| Mon, 24 Mar 2014 19:06:20 +0100 |
wenzelm |
removed unused 'ax_specification', to give 'specification' a chance to become localized;
|
file |
diff |
annotate
|
| Fri, 28 Feb 2014 17:54:52 +0100 |
traytel |
load Metis a little later
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed 'nat_{case,rec}' to '{case,rec}_nat'
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 23:07:23 +0100 |
blanchet |
moved 'bacc' back to 'Enum' (cf. 744934b818c7) -- reduces baggage loaded by 'Hilbert_Choice'
|
file |
diff |
annotate
|