#
c5b95729 |
|
08-Mar-2020 |
haftmann <none@none> |
more frugal simp rules for bit operations; more pervasive use of bit selector --HG-- extra : rebase_source : 09f56fd30f4ab8ae84811041575772264eb330b3
|
#
0635ff6c |
|
25-Feb-2020 |
paulson <lp15@cam.ac.uk> |
Moved a number of general-purpose lemmas into HOL
|
#
fe5914fe |
|
16-Feb-2020 |
nipkow <none@none> |
lemmas about "card A = 2"; prefer iff to implications
|
#
ec78305b |
|
09-Dec-2019 |
paulson <lp15@cam.ac.uk> |
a few new and tidier proofs (mostly about finite sets)
|
#
6e12876d |
|
26-Nov-2019 |
paulson <lp15@cam.ac.uk> |
Rearrangement of material in Complex_Analysis_Basics, which contained much that had nothing to do with complex analysis.
|
#
3b6cecbe |
|
09-Nov-2019 |
haftmann <none@none> |
bit shifts as class operations
|
#
a4784f6f |
|
09-Oct-2019 |
haftmann <none@none> |
dedicated fact collections for algebraic simplification rules potentially splitting goals --HG-- extra : rebase_source : ebbd8d0c13409f8fb536c42910e904c24e43dbe6
|
#
c56a85fc |
|
23-Sep-2019 |
paulson <lp15@cam.ac.uk> |
More type class generalisations. Note that linorder_antisym_conv1 and linorder_antisym_conv2 no longer exist.
|
#
a19a024d |
|
23-Sep-2019 |
paulson <lp15@cam.ac.uk> |
Generalisation of many theorems to a more abstract type class (suggested by Mr Anonymous)
|
#
a1f8bb2d |
|
18-Sep-2019 |
paulson <lp15@cam.ac.uk> |
imported new material mostly due to Sébastien Gouëzel
|
#
e6ca3b44 |
|
17-Jul-2019 |
paulson <lp15@cam.ac.uk> |
a few new lemmas and a bit of tidying
|
#
6ee2be1e |
|
14-Jun-2019 |
haftmann <none@none> |
slightly more specialized name for type class
|
#
35216754 |
|
10-Apr-2019 |
paulson <lp15@cam.ac.uk> |
Fixing the main Homology theory; also moving a lot of sum/prod lemmas into their generic context
|
#
48a391b7 |
|
10-Apr-2019 |
paulson <lp15@cam.ac.uk> |
The last big tranche of Homology material: invariance of domain; renamings to use generic sum/prod lemmas from their locale
|
#
e977f1fa |
|
31-Jan-2019 |
haftmann <none@none> |
proper congruence rule for image operator --HG-- extra : rebase_source : 71f59936260619419f4d3f7f86d1b930bc771065
|
#
083015db |
|
21-Jan-2019 |
paulson <lp15@cam.ac.uk> |
new material about summations and powers, along with some tweaks
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
05936fb0 |
|
23-Dec-2018 |
haftmann <none@none> |
more rules
|
#
e01498ae |
|
10-Nov-2018 |
haftmann <none@none> |
replaced some ancient ASCII syntax
|
#
576b136c |
|
05-Nov-2018 |
nipkow <none@none> |
simplified proof, moved lemma, added lemma
|
#
8dddbfd5 |
|
27-Oct-2018 |
nipkow <none@none> |
moved lemmas
|
#
e5dab920 |
|
25-Oct-2018 |
haftmann <none@none> |
more and generalized lemmas
|
#
cc37beb1 |
|
24-Sep-2018 |
nipkow <none@none> |
Prefix form of infix with * on either side no longer needs special treatment because (* and *) are no longer comment brackets in terms.
|
#
685c0eec |
|
12-Jul-2018 |
paulson <lp15@cam.ac.uk> |
de-applying (mostly Set_Interval)
|
#
2386b68a |
|
03-Jun-2018 |
paulson <lp15@cam.ac.uk> |
infinite product material
|
#
27050edb |
|
01-May-2018 |
paulson <lp15@cam.ac.uk> |
type class generalisations; some work on infinite products
|
#
ec4ba366 |
|
15-Apr-2018 |
haftmann <none@none> |
more and generalized lemmas --HG-- extra : rebase_source : 427f9ca2975f1d4f8635e3509a6d1045335cf09a
|
#
0893d241 |
|
21-Mar-2018 |
haftmann <none@none> |
prefer convention to place operation name before type name
|
#
0b6326bb |
|
10-Mar-2018 |
haftmann <none@none> |
abstract algebraic bit operations --HG-- extra : rebase_source : 10402190e8858b0ea47b7ac7f91671a9935921ae
|
#
78eb1fe1 |
|
25-Feb-2018 |
immler <none@none> |
moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements
|
#
7f370351 |
|
22-Feb-2018 |
immler <none@none> |
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
|
#
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
#
5385dbfa |
|
16-Jan-2018 |
wenzelm <none@none> |
standardized towards new-style formal comments: isabelle update_comments;
|
#
fa1f0d8b |
|
13-Jan-2018 |
haftmann <none@none> |
restored naming of lemmas after corresponding constants
|
#
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
#
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
#
711c1878 |
|
30-Oct-2017 |
haftmann <none@none> |
tuned some proofs and added some lemmas --HG-- extra : rebase_source : ad93f195ceb7a124396a911453e61f00f52999be
|
#
eda74618 |
|
09-Oct-2017 |
haftmann <none@none> |
tuned imports --HG-- extra : rebase_source : bc9797cb892085195c2d8662a7ca3896dd1e5011
|
#
62e3d173 |
|
23-Aug-2017 |
nipkow <none@none> |
added lemma
|
#
d244f158 |
|
25-Apr-2017 |
paulson <lp15@cam.ac.uk> |
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
|
#
1e533d09 |
|
16-Mar-2017 |
paulson <lp15@cam.ac.uk> |
Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.
|
#
c8cee3c6 |
|
04-Jan-2017 |
paulson <lp15@cam.ac.uk> |
Many new theorems, and more tidying
|
#
593ff4b4 |
|
17-Oct-2016 |
nipkow <none@none> |
setprod -> prod
|
#
351cc2e6 |
|
17-Oct-2016 |
nipkow <none@none> |
setsum -> sum
|
#
657eacc4 |
|
30-Sep-2016 |
paulson <lp15@cam.ac.uk> |
new material on paths, etc. Also rationalisation
|
#
d85aaeb8 |
|
21-Sep-2016 |
wenzelm <none@none> |
raw control symbols are superseded by Latex.embed_raw;
|
#
9a8c3fb3 |
|
19-Sep-2016 |
fleury <Mathias.Fleury@mpi-inf.mpg.de> |
left_distrib ~> distrib_right, right_distrib ~> distrib_left
|
#
6d0b05b4 |
|
18-Sep-2016 |
wenzelm <none@none> |
tuned proofs;
|
#
1e83a38a |
|
15-Sep-2016 |
paulson <lp15@cam.ac.uk> |
simple new lemmas, mostly about sets
|
#
c6fb3931 |
|
25-Aug-2016 |
Manuel Eberl <eberlm@in.tum.de> |
More analysis lemmas
|
#
14001a0d |
|
22-Jul-2016 |
wenzelm <none@none> |
tuned proofs -- avoid unstructured calculation;
|
#
a70bd0e1 |
|
09-Jul-2016 |
haftmann <none@none> |
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat * * * more rules for setsum, setprod on intervals
|
#
0f0a91d1 |
|
02-Jul-2016 |
haftmann <none@none> |
more theorems
|
#
1e23b491 |
|
16-Jun-2016 |
eberlm <none@none> |
Various additions to polynomials, FPSs, Gamma function
|
#
9ebcfa62 |
|
27-May-2016 |
wenzelm <none@none> |
tuned proofs;
|
#
b5509112 |
|
23-May-2016 |
paulson <lp15@cam.ac.uk> |
Lots of new material for multivariate analysis
|
#
94ba250a |
|
17-May-2016 |
eberlm <none@none> |
Moved material from AFP/Randomised_Social_Choice to distribution
|
#
1daf8189 |
|
13-May-2016 |
wenzelm <none@none> |
eliminated use of empty "assms";
|
#
772cb5d0 |
|
01-Apr-2016 |
wenzelm <none@none> |
explicit property for unbreakable block;
|
#
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
#
259fcfd2 |
|
22-Feb-2016 |
paulson <lp15@cam.ac.uk> |
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
|
#
cef8f2ad |
|
10-Feb-2016 |
hoelzl <none@none> |
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids. --HG-- extra : rebase_source : 54bd3e5fcde04ef38241be91231c48d078b850f2
|
#
c84c7ed2 |
|
08-Feb-2016 |
hoelzl <none@none> |
instantiate topologies for nat, int and enat --HG-- extra : rebase_source : 2320da44d4913f441c671ef425945fac6d4381c9
|
#
6688eecc |
|
17-Feb-2016 |
haftmann <none@none> |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
#
e89ec887 |
|
11-Jan-2016 |
eberlm <none@none> |
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
|
#
0bfb73b6 |
|
28-Dec-2015 |
wenzelm <none@none> |
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
|
#
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
2f29d214 |
|
29-Oct-2015 |
eberlm <none@none> |
added many small lemmas about setsum/setprod/powr/...
|
#
607ae3e3 |
|
09-Oct-2015 |
wenzelm <none@none> |
discontinued specific HTML syntax;
|
#
33d48711 |
|
21-Sep-2015 |
paulson <none@none> |
new lemmas and movement of lemmas into place
|
#
5cdcf3d3 |
|
28-Jul-2015 |
paulson <lp15@cam.ac.uk> |
the Cauchy integral theorem and related material
|
#
a219c2a1 |
|
20-Jul-2015 |
paulson <none@none> |
new material for multivariate analysis, etc.
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
7d3b4baf |
|
30-Jun-2015 |
paulson <lp15@cam.ac.uk> |
Useful lemmas. The theorem concerning swapping the variables in a double integral.
|
#
7f5a6758 |
|
26-Jun-2015 |
wenzelm <none@none> |
proper spacing, as for other syntax for these symbols;
|
#
d20797ec |
|
30-Apr-2015 |
paulson <lp15@cam.ac.uk> |
tidying some messy proofs
|
#
587e133b |
|
28-Apr-2015 |
paulson <lp15@cam.ac.uk> |
New material about complex transcendental functions (especially Ln, Arg) and polynomials
|
#
d6db773a |
|
11-Apr-2015 |
paulson <lp15@cam.ac.uk> |
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
|
#
3b8affd9 |
|
20-Jan-2015 |
hoelzl <none@none> |
generalized sum_diff_distrib to setsum_subtractf_nat --HG-- extra : rebase_source : 713d89f4f5743dee1259a32a3ec3dc08984cd6bf
|
#
ff53cb2b |
|
13-Nov-2014 |
hoelzl <none@none> |
import general theorems from AFP/Markov_Models
|
#
61a407a0 |
|
11-Nov-2014 |
noschinl <none@none> |
add forgotten lemma
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
38907e37 |
|
05-Jul-2014 |
haftmann <none@none> |
prefer ac_simps collections over separate name bindings for add and mult
|
#
e46c07fd |
|
04-Jul-2014 |
haftmann <none@none> |
reduced name variants for assoc and commute on plus and mult
|
#
d37dfba9 |
|
30-Jun-2014 |
hoelzl <none@none> |
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs --HG-- extra : rebase_source : 8664c1d86ed72607199cc8197a480070514ae330
|
#
6c0336e5 |
|
30-Jun-2014 |
hoelzl <none@none> |
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure --HG-- extra : rebase_source : 03b2468f7b324b9d8add229ae59776b447283141
|
#
bf4e83d3 |
|
28-Jun-2014 |
haftmann <none@none> |
fact consolidation
|
#
43e1aec7 |
|
30-May-2014 |
hoelzl <none@none> |
introduce more powerful reindexing rules for big operators
|
#
c4c942c6 |
|
29-May-2014 |
paulson <lp15@cam.ac.uk> |
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
|
#
0561a579 |
|
13-May-2014 |
hoelzl <none@none> |
clean up Lebesgue integration
|
#
d749d414 |
|
09-Apr-2014 |
hoelzl <none@none> |
field_simps: better support for negation and division, and power
|
#
87b8d15e |
|
30-Mar-2014 |
hoelzl <none@none> |
add rules about infinity of intervals
|
#
52d226b9 |
|
21-Mar-2014 |
paulson <lp15@cam.ac.uk> |
a few new lemmas and generalisations of old ones
|
#
cd1dc8a6 |
|
19-Mar-2014 |
paulson <lp15@cam.ac.uk> |
New complex analysis material
|
#
d6283f3b |
|
18-Mar-2014 |
hoelzl <none@none> |
fix HOL-NSA; move lemmas
|
#
4cda3a80 |
|
18-Mar-2014 |
hoelzl <none@none> |
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
|
#
9a3670d8 |
|
24-Feb-2014 |
paulson <lp15@cam.ac.uk> |
Lemmas about Reals, norm, etc., and cleaner variants of existing ones
|
#
0f82e936 |
|
24-Feb-2014 |
paulson <lp15@cam.ac.uk> |
A few lemmas about summations, etc.
|
#
89444e58 |
|
02-Feb-2014 |
paulson <lp15@cam.ac.uk> |
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
|
#
b96e01d8 |
|
25-Jan-2014 |
wenzelm <none@none> |
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
|
#
2fc85925 |
|
20-Jan-2014 |
blanchet <none@none> |
moved 'bacc' back to 'Enum' (cf. 744934b818c7) -- reduces baggage loaded by 'Hilbert_Choice'
|
#
d46ef5de |
|
20-Jan-2014 |
blanchet <none@none> |
moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain --HG-- rename : src/HOL/FunDef.thy => src/HOL/Fun_Def.thy
|
#
0138e8ab |
|
28-Nov-2013 |
blanchet <none@none> |
cleaned up indirect dependency
|
#
03633065 |
|
18-Oct-2013 |
blanchet <none@none> |
killed most "no_atp", to make Sledgehammer more complete
|
#
7237bdd9 |
|
02-Sep-2013 |
wenzelm <none@none> |
tuned proofs -- clarified flow of facts wrt. calculation;
|
#
0ad1a5d3 |
|
27-Aug-2013 |
hoelzl <none@none> |
renamed inner_dense_linorder to dense_linorder --HG-- extra : rebase_source : a7a9c602f6d7437d9632ccdffa7d3b6eaafc2d01
|
#
1612e9ff |
|
25-Jul-2013 |
haftmann <none@none> |
factored syntactic type classes for bot and top (by Alessandro Coglio)
|
#
d820eec9 |
|
15-Jun-2013 |
haftmann <none@none> |
lifting for primitive definitions; explicit conversions from and to lists of coefficients, used for generated code; replaced recursion operator poly_rec by fold_coeffs, preferring function definitions for non-trivial recursions; prefer pre-existing gcd operation for gcd
|
#
3f8c7efb |
|
05-Mar-2013 |
nipkow <none@none> |
more lemmas about intervals
|
#
31f651ff |
|
19-Feb-2013 |
hoelzl <none@none> |
split dense into inner_dense_order and no_top/no_bot
|
#
cc794fdb |
|
19-Feb-2013 |
hoelzl <none@none> |
move auxiliary lemmas from Library/Extended_Reals to HOL image
|
#
8434f21c |
|
15-Feb-2013 |
Andreas Lochbihler <none@none> |
added lemma
|
#
a1f00aa7 |
|
31-Jan-2013 |
hoelzl <none@none> |
introduce order topology
|
#
130f2067 |
|
07-Dec-2012 |
hoelzl <none@none> |
add Int_atMost
|
#
109489f9 |
|
24-May-2012 |
wenzelm <none@none> |
tuned proofs;
|
#
096befcf |
|
03-Apr-2012 |
huffman <none@none> |
modernized obsolete old-style theory name with proper new-style underscore --HG-- rename : src/HOL/SetInterval.thy => src/HOL/Set_Interval.thy
|