| #
f4f1a444 |
|
15-May-2018 |
immler <none@none> |
move FuncSet back to HOL-Library (amending 493b818e8e10)
--HG--
rename : src/HOL/FuncSet.thy => src/HOL/Library/FuncSet.thy
|
| #
e04b7748 |
|
02-May-2018 |
immler <none@none> |
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
--HG--
rename : src/HOL/Library/FuncSet.thy => src/HOL/FuncSet.thy
|
| #
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
| #
4ed5daad |
|
04-Nov-2017 |
wenzelm <none@none> |
prefer main entry points of HOL;
|
| #
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
| #
593ff4b4 |
|
17-Oct-2016 |
nipkow <none@none> |
setprod -> prod
|
| #
ee8e8234 |
|
06-Oct-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
3e14dd10 |
|
16-Mar-2015 |
paulson <lp15@cam.ac.uk> |
The factorial function, "fact", now has type "nat => 'a"
|
| #
b9259bee |
|
10-Mar-2015 |
paulson <lp15@cam.ac.uk> |
renaming HOL/Fact.thy -> Binomial.thy
--HG--
rename : src/HOL/Fact.thy => src/HOL/Binomial.thy
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
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
|
| #
ae1af368 |
|
07-Jun-2011 |
bulwahn <none@none> |
renaming the formalisation of the birthday problem to a proper English name
--HG--
rename : src/HOL/ex/Birthday_Paradoxon.thy => src/HOL/ex/Birthday_Paradox.thy
|