| #
977ba149 |
|
13-Mar-2020 |
wenzelm <none@none> |
proper escape for literal single quotes;
|
| #
ab32308e |
|
21-Jan-2019 |
paulson <lp15@cam.ac.uk> |
renamings and new material
|
| #
504acaca |
|
14-Jan-2019 |
haftmann <none@none> |
tuned proofs
|
| #
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
09859749 |
|
18-Nov-2018 |
haftmann <none@none> |
removed legacy input syntax
|
| #
97b2ecf5 |
|
08-Nov-2018 |
haftmann <none@none> |
removed relics of ASCII syntax for indexed big operators
|
| #
8bc115f8 |
|
08-May-2018 |
paulson <lp15@cam.ac.uk> |
one tiny fix
|
| #
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
| #
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
| #
02200082 |
|
11-Jul-2017 |
Lars Hupel <lars.hupel@mytum.de> |
fmaps are countable
|
| #
9592ed4f |
|
10-Jul-2017 |
Lars Hupel <lars.hupel@mytum.de> |
finite sets are countable
--HG--
extra : amend_source : cea729a1e159fa171d76020f2bccdb82281d87dc
|
| #
7f0566a2 |
|
15-Jun-2017 |
paulson <lp15@cam.ac.uk> |
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
|
| #
b7255f21 |
|
04-Nov-2016 |
hoelzl <none@none> |
HOL-Probability: fix import path in Fin_Map
|
| #
bef11030 |
|
15-Sep-2016 |
Lars Hupel <lars.hupel@mytum.de> |
new type for finite maps; use it in HOL-Probability
|
| #
2361d31f |
|
02-Aug-2016 |
immler <none@none> |
more natural definition of type finmap
|
| #
a2bc0021 |
|
25-Apr-2016 |
wenzelm <none@none> |
eliminated old 'def';
tuned comments;
|
| #
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
| #
6688eecc |
|
17-Feb-2016 |
haftmann <none@none> |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
| #
ec265e34 |
|
08-Jan-2016 |
hoelzl <none@none> |
fix code generation for uniformity: uniformity is a non-computable pure data.
|
| #
da01cc11 |
|
08-Jan-2016 |
hoelzl <none@none> |
add uniform spaces
|
| #
7a1f0bb7 |
|
30-Dec-2015 |
wenzelm <none@none> |
clarified print modes;
|
| #
82353fd1 |
|
30-Dec-2015 |
wenzelm <none@none> |
more symbols;
|
| #
6d3e0a15 |
|
29-Dec-2015 |
wenzelm <none@none> |
more symbols;
|
| #
8e83c9d2 |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
607ae3e3 |
|
09-Oct-2015 |
wenzelm <none@none> |
discontinued specific HTML syntax;
|
| #
4ca0fb8f |
|
04-Dec-2014 |
hoelzl <none@none> |
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
|
| #
ce7c103d |
|
23-Nov-2014 |
hoelzl <none@none> |
add congruence solver to measurability prover
--HG--
extra : rebase_source : 77341231f7d3ba19edd6c5865552541156a3dd71
|
| #
f8e9ab7b |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header;
|
| #
b1300353 |
|
23-Apr-2014 |
hoelzl <none@none> |
remove add_eq_zero_iff, it is replaced by add_nonneg_eq_0_iff; also removes it from the simpset
|
| #
430dcf36 |
|
19-Mar-2014 |
wenzelm <none@none> |
tuned -- no need for slightly obscure "local" prefix;
|
| #
7237bdd9 |
|
02-Sep-2013 |
wenzelm <none@none> |
tuned proofs -- clarified flow of facts wrt. calculation;
|
| #
06329277 |
|
13-Aug-2013 |
wenzelm <none@none> |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
| #
4a0d6c03 |
|
09-Apr-2013 |
hoelzl <none@none> |
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
|
| #
d4cae3bf |
|
23-Mar-2013 |
haftmann <none@none> |
fundamental revision of big operators on sets
|
| #
8be046c2 |
|
22-Mar-2013 |
hoelzl <none@none> |
move first_countable_topology to the HOL image
|
| #
c1893073 |
|
05-Mar-2013 |
hoelzl <none@none> |
use generate_topology for second countable topologies, does not require intersection stable basis
|
| #
8176c074 |
|
13-Feb-2013 |
immler <none@none> |
eliminated union_closed_basis; cleanup Fin_Map
|
| #
19903ad6 |
|
13-Feb-2013 |
immler <none@none> |
fine grained instantiations
|
| #
a5f43f66 |
|
13-Feb-2013 |
immler <none@none> |
use maximum norm for type finmap
|
| #
23578d8d |
|
14-Jan-2013 |
hoelzl <none@none> |
renamed countable_basis_space to second_countable_topology
--HG--
extra : rebase_source : 1287b8162fd3311e5100ce1912cb58896edfb3a5
|
| #
c319b7be |
|
28-Nov-2012 |
wenzelm <none@none> |
tuned syntax, potentially more robust;
|
| #
21822db4 |
|
27-Nov-2012 |
immler <none@none> |
based countable topological basis on Countable_Set
--HG--
extra : rebase_source : 326111b06e0d89bbbef5c168b8314ab6023d8fb2
|
| #
ba5f9f86 |
|
27-Nov-2012 |
immler <none@none> |
qualified interpretation of sigma_algebra, to avoid name clashes
--HG--
extra : rebase_source : aaeab4e40463c23ef5a5a07ee360db0335376105
|
| #
a0853ad0 |
|
19-Nov-2012 |
hoelzl <none@none> |
tuned FinMap
--HG--
extra : rebase_source : 8291b62bb69ca72f48d94c100f98e12c28076978
|
| #
2e3f9613 |
|
18-Nov-2012 |
hoelzl <none@none> |
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
--HG--
extra : rebase_source : e65af8d29763871aedf04aed10bdeb869effca0b
|
| #
bea763ee |
|
16-Nov-2012 |
hoelzl <none@none> |
renamed measurable_compose -> measurable_finmap_compose, clashed with Sigma_Algebra.measurable_compose
|
| #
2c4703d5 |
|
16-Nov-2012 |
immler <none@none> |
allow arbitrary enumerations of basis in locale for generation of borel sets
|
| #
08adb1df |
|
15-Nov-2012 |
immler <none@none> |
corrected headers
|
| #
de502a80 |
|
15-Nov-2012 |
immler <none@none> |
added projective limit;
proof is based on auxiliary type finmap::polish_space
--HG--
extra : rebase_source : 08af71f8dedbbe8cb079512c97691cc68592d86f
|