isabelle: src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy@3e491e34a62e (annotated)

33267 8fb01a2f9406 tuned initial session setup; wenzelm parents: 33175 diff changeset	1	theory Multivariate_Analysis
59453 4736ff5a41d8 moved bcontfun from AFP/Ordinary_Differential_Equations hoelzl parents: 56370 diff changeset	2	imports
4736ff5a41d8 moved bcontfun from AFP/Ordinary_Differential_Equations hoelzl parents: 56370 diff changeset	3	Fashoda
4736ff5a41d8 moved bcontfun from AFP/Ordinary_Differential_Equations hoelzl parents: 56370 diff changeset	4	Extended_Real_Limits
4736ff5a41d8 moved bcontfun from AFP/Ordinary_Differential_Equations hoelzl parents: 56370 diff changeset	5	Determinants
4736ff5a41d8 moved bcontfun from AFP/Ordinary_Differential_Equations hoelzl parents: 56370 diff changeset	6	Ordered_Euclidean_Space
4736ff5a41d8 moved bcontfun from AFP/Ordinary_Differential_Equations hoelzl parents: 56370 diff changeset	7	Complex_Analysis_Basics
4736ff5a41d8 moved bcontfun from AFP/Ordinary_Differential_Equations hoelzl parents: 56370 diff changeset	8	Bounded_Continuous_Function
60812 8fff64349793 added theory Uniform_Limit immler parents: 59453 diff changeset	9	Uniform_Limit
60987 ea00d17eba3b The Stone-Weierstrass theorem paulson <lp15@cam.ac.uk> parents: 60812 diff changeset	10	Weierstrass
33175 2083bde13ce1 distinguished session for multivariate analysis himmelma parents: diff changeset	11	begin
2083bde13ce1 distinguished session for multivariate analysis himmelma parents: diff changeset	12
2083bde13ce1 distinguished session for multivariate analysis himmelma parents: diff changeset	13	end

author	paulson
	Mon, 21 Sep 2015 19:52:13 +0100
changeset 61204	3e491e34a62e
parent 60987	ea00d17eba3b
child 61243	44b2d133063e
permissions	-rw-r--r--