| Thu, 23 Jun 2022 19:29:22 +0200 |
desharna |
changed argument order of mono_on and strict_mono_on to uniformize with monotone_on and other predicates
|
file |
diff |
annotate
|
| Thu, 05 Aug 2021 07:12:49 +0000 |
haftmann |
clarified abstract and concrete boolean algebras
|
file |
diff |
annotate
|
| Wed, 05 May 2021 16:09:02 +0000 |
haftmann |
tuned theory structure
|
file |
diff |
annotate
|
| Sun, 11 Apr 2021 07:35:24 +0000 |
haftmann |
collected combinatorial material
|
file |
diff |
annotate
|
| Thu, 11 Mar 2021 07:05:38 +0000 |
haftmann |
avoid name clash
|
file |
diff |
annotate
|
| Sun, 28 Feb 2021 20:13:07 +0000 |
haftmann |
lemma diffusion
|
file |
diff |
annotate
|
| 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
|
| Thu, 16 Jan 2014 18:26:41 +0100 |
blanchet |
dissolved 'Fun_More_FP' (a BNF dependency)
|
file |
diff |
annotate
|
| Sun, 15 Dec 2013 15:10:14 +0100 |
haftmann |
more algebraic terminology for theories about big operators
|
file |
diff |
annotate
|
| Mon, 25 Nov 2013 10:14:29 +0100 |
traytel |
eliminated dependence of BNF on Infinite_Set by moving 3 theorems from the latter to Main
|
file |
diff |
annotate
|
| Sun, 10 Nov 2013 15:05:06 +0100 |
haftmann |
qualifed popular user space names
|
file |
diff |
annotate
|
| Sat, 25 May 2013 15:37:53 +0200 |
wenzelm |
syntax translations always depend on context;
|
file |
diff |
annotate
|
| Fri, 16 Nov 2012 19:14:23 +0100 |
hoelzl |
moved (b)choice_iff(') to Hilbert_Choice
|
file |
diff |
annotate
|
| Sat, 20 Oct 2012 09:12:16 +0200 |
haftmann |
moved quite generic material from theory Enum to more appropriate places
|
file |
diff |
annotate
|
| Mon, 08 Oct 2012 12:03:49 +0200 |
haftmann |
consolidated names of theorems on composition;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Thu, 24 May 2012 17:25:53 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 22:08:53 +0100 |
wenzelm |
declare command keywords via theory header, including strict checking outside Pure;
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 21:07:10 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 17:07:33 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 13:31:16 +0200 |
wenzelm |
explicit structure Syntax_Trans;
|
file |
diff |
annotate
|
| Tue, 23 Nov 2010 14:14:17 +0100 |
hoelzl |
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 10:34:33 +0100 |
hoelzl |
Replace surj by abbreviation; remove surj_on.
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 10:59:12 +0200 |
blanchet |
got rid of overkill "meson_choice" attribute;
|
file |
diff |
annotate
|
| Mon, 04 Oct 2010 21:55:54 +0200 |
blanchet |
remove Meson from Hilbert_Choice
|
file |
diff |
annotate
|
| Fri, 01 Oct 2010 14:01:29 +0200 |
blanchet |
added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 11:29:02 +0200 |
blanchet |
use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 13:40:23 +0100 |
haftmann |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 14:21:44 -0800 |
huffman |
get rid of many duplicate simp rule warnings
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 23:00:22 +0100 |
wenzelm |
modernized translations;
|
file |
diff |
annotate
|
| Thu, 22 Oct 2009 09:27:48 +0200 |
nipkow |
inv_onto -> inv_into
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 13:20:42 +0200 |
nipkow |
added inv_def for compatibility as a lemma
|
file |
diff |
annotate
|
| Sun, 18 Oct 2009 12:07:25 +0200 |
nipkow |
Inv -> inv_onto, inv abbr. inv_onto UNIV.
|
file |
diff |
annotate
|
| Fri, 19 Jun 2009 17:23:21 +0200 |
haftmann |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file |
diff |
annotate
|
| Thu, 04 Jun 2009 15:28:58 +0200 |
haftmann |
dropped legacy ML bindings; tuned
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 16:23:43 +0200 |
haftmann |
added/moved lemmas by Andreas Lochbihler
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 11:03:42 +0100 |
haftmann |
Plain, Main form meeting points in import hierarchy
|
file |
diff |
annotate
|
| Wed, 06 Aug 2008 13:57:25 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Fri, 25 Apr 2008 15:30:33 +0200 |
krauss |
Merged theories about wellfoundedness into one: Wellfounded.thy
|
file |
diff |
annotate
|
| Mon, 07 Apr 2008 15:37:27 +0200 |
paulson |
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
|
file |
diff |
annotate
|
| Thu, 20 Mar 2008 12:01:09 +0100 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Thu, 21 Feb 2008 17:33:58 +0100 |
nipkow |
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
|
file |
diff |
annotate
|
| Fri, 15 Feb 2008 16:09:12 +0100 |
haftmann |
<= and < on nat no longer depend on wellfounded relations
|
file |
diff |
annotate
|
| Wed, 20 Jun 2007 14:38:24 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Sun, 15 Apr 2007 14:31:44 +0200 |
wenzelm |
replaced axioms/finalconsts by proper axiomatization;
|
file |
diff |
annotate
|
| Thu, 04 Jan 2007 17:55:12 +0100 |
paulson |
improvements to proof reconstruction. Some files loaded in a different order
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 13:48:29 +0100 |
wenzelm |
removed theory NatArith (now part of Nat);
|
file |
diff |
annotate
|
| Fri, 13 Oct 2006 18:15:18 +0200 |
berghofe |
Adapted to changes in FixedPoint theory.
|
file |
diff |
annotate
|
| Tue, 13 Dec 2005 15:27:43 +0100 |
paulson |
removal of functional reflexivity axioms
|
file |
diff |
annotate
|
| Tue, 18 Oct 2005 17:59:26 +0200 |
wenzelm |
added lemma exE_some (from specification_package.ML);
|
file |
diff |
annotate
|
| Thu, 29 Sep 2005 00:58:55 +0200 |
wenzelm |
more finalconsts;
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 17:44:53 +0200 |
paulson |
comment
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 15:06:20 +0200 |
paulson |
generlization of some "nat" theorems
|
file |
diff |
annotate
|
| Fri, 24 Jun 2005 17:25:10 +0200 |
paulson |
meson method taking an argument list
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Tue, 19 Oct 2004 18:18:45 +0200 |
paulson |
converted some induct_tac to induct
|
file |
diff |
annotate
|
| Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
| Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|