| #
97b2ecf5 |
|
08-Nov-2018 |
haftmann <none@none> |
removed relics of ASCII syntax for indexed big operators
|
| #
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;
|
| #
f63c7c02 |
|
20-Oct-2016 |
hoelzl <none@none> |
HOL-Probability: move stopping time from AFP/Markov_Models
|
| #
fad39d02 |
|
30-Sep-2016 |
hoelzl <none@none> |
HOL-Probability: more about probability, prepare for Markov processes in the AFP
--HG--
extra : rebase_source : f90e6cf5c47f7a2604d0eeacaf0181f3cfe64a14
|
| #
188a9299 |
|
16-Jun-2016 |
hoelzl <none@none> |
Probability: show that measures form a complete lattice
--HG--
extra : rebase_source : bb357b4daf07004fdbda6bdf8f08655e7e37c742
|
| #
474064bd |
|
09-Dec-2015 |
paulson <lp15@cam.ac.uk> |
sorted out eventually_mono
|
| #
8e83c9d2 |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
5012105f |
|
13-Sep-2015 |
wenzelm <none@none> |
tuned proofs -- less legacy;
|
| #
66005bbd |
|
04-May-2015 |
hoelzl <none@none> |
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
--HG--
extra : rebase_source : 6c7faec3b6fc45b9da856e08add46f99a0b483b7
|
| #
2dd36018 |
|
04-Dec-2014 |
hoelzl <none@none> |
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
--HG--
extra : rebase_source : 8c7131ba8a4f577186bc3393e7116b70e552dd7e
|
| #
ce7c103d |
|
23-Nov-2014 |
hoelzl <none@none> |
add congruence solver to measurability prover
--HG--
extra : rebase_source : 77341231f7d3ba19edd6c5865552541156a3dd71
|
| #
ff53cb2b |
|
13-Nov-2014 |
hoelzl <none@none> |
import general theorems from AFP/Markov_Models
|
| #
cd244101 |
|
07-Oct-2014 |
hoelzl <none@none> |
move Stream theory from Datatype_Examples to Library
--HG--
rename : src/HOL/Datatype_Examples/Stream.thy => src/HOL/Library/Stream.thy
extra : amend_source : e73f82c1bd2e07cabeaa7ac3f08f44cad2f2cec6
|
| #
e46f9abe |
|
07-Oct-2014 |
hoelzl <none@none> |
add Giry monad
--HG--
extra : rebase_source : 3ceb1c0fa2e24cb05e37856566255a7b56f80af7
|
| #
8458b574 |
|
06-Oct-2014 |
hoelzl <none@none> |
add measure space for (coinductive) streams
|