--- a/src/HOL/Analysis/Analysis.thy Wed Jan 16 18:14:02 2019 -0500
+++ b/src/HOL/Analysis/Analysis.thy Wed Jan 16 19:34:48 2019 -0500
@@ -1,5 +1,20 @@
theory Analysis
-imports
+ imports
+ (* Linear Algebra *)
+ Convex
+ Determinants
+ (* Topology *)
+ Connected
+ (* Functional Analysis *)
+ Elementary_Normed_Spaces
+ Norm_Arith
+ (* Vector Analysis *)
+ Convex_Euclidean_Space
+ (* Measure and Integration Theory *)
+ Ball_Volume
+ Integral_Test
+ Improper_Integral
+ (* Unsorted *)
Lebesgue_Integral_Substitution
Improper_Integral
Embed_Measure
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Wed Jan 16 18:14:02 2019 -0500
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Wed Jan 16 19:34:48 2019 -0500
@@ -4,13 +4,15 @@
Author: Brian Huffman, Portland State University
*)
-section \<open>Elementary Metric Spaces\<close>
+chapter \<open>Functional Analysis\<close>
theory Elementary_Metric_Spaces
imports
Abstract_Topology_2
begin
+section \<open>Elementary Metric Spaces\<close>
+
subsection \<open>Open and closed balls\<close>
definition%important ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
--- a/src/HOL/Analysis/Elementary_Topology.thy Wed Jan 16 18:14:02 2019 -0500
+++ b/src/HOL/Analysis/Elementary_Topology.thy Wed Jan 16 19:34:48 2019 -0500
@@ -4,7 +4,7 @@
Author: Brian Huffman, Portland State University
*)
-section \<open>Elementary Topology\<close>
+chapter \<open>Topology\<close>
theory Elementary_Topology
imports
@@ -14,6 +14,8 @@
begin
+section \<open>Elementary Topology\<close>
+
subsection \<open>TODO: move?\<close>
lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)"
--- a/src/HOL/Analysis/L2_Norm.thy Wed Jan 16 18:14:02 2019 -0500
+++ b/src/HOL/Analysis/L2_Norm.thy Wed Jan 16 19:34:48 2019 -0500
@@ -2,12 +2,14 @@
Author: Brian Huffman, Portland State University
*)
-section \<open>L2 Norm\<close>
+chapter \<open>Linear Algebra\<close>
theory L2_Norm
imports Complex_Main
begin
+section \<open>L2 Norm\<close>
+
definition%important L2_set :: "('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> real" where
"L2_set f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
--- a/src/HOL/Analysis/Sigma_Algebra.thy Wed Jan 16 18:14:02 2019 -0500
+++ b/src/HOL/Analysis/Sigma_Algebra.thy Wed Jan 16 19:34:48 2019 -0500
@@ -5,7 +5,7 @@
translated by Lawrence Paulson.
*)
-section \<open>Sigma Algebra\<close>
+chapter \<open>Measure and Integration Theory\<close>
theory Sigma_Algebra
imports
@@ -17,6 +17,9 @@
"HOL-Library.Disjoint_Sets"
begin
+
+section \<open>Sigma Algebra\<close>
+
text \<open>Sigma algebras are an elementary concept in measure
theory. To measure --- that is to integrate --- functions, we first have
to measure sets. Unfortunately, when dealing with a large universe,
--- a/src/HOL/Analysis/Starlike.thy Wed Jan 16 18:14:02 2019 -0500
+++ b/src/HOL/Analysis/Starlike.thy Wed Jan 16 19:34:48 2019 -0500
@@ -5,13 +5,14 @@
Author: Armin Heller, TU Muenchen
Author: Johannes Hoelzl, TU Muenchen
*)
-
-section \<open>Line Segments\<close>
+chapter \<open>Unsorted\<close>
theory Starlike
imports Convex_Euclidean_Space
begin
+section \<open>Line Segments\<close>
+
subsection \<open>Midpoint\<close>
definition%important midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a"
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Wed Jan 16 18:14:02 2019 -0500
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Wed Jan 16 19:34:48 2019 -0500
@@ -4,7 +4,7 @@
Author: Brian Huffman, Portland State University
*)
-section \<open>Elementary Topology in Euclidean Space\<close>
+chapter \<open>Vector Analysis\<close>
theory Topology_Euclidean_Space
imports
@@ -13,6 +13,8 @@
Norm_Arith
begin
+section \<open>Elementary Topology in Euclidean Space\<close>
+
lemma euclidean_dist_l2:
fixes x y :: "'a :: euclidean_space"
shows "dist x y = L2_set (\<lambda>i. dist (x \<bullet> i) (y \<bullet> i)) Basis"
--- a/src/HOL/Analysis/document/root.tex Wed Jan 16 18:14:02 2019 -0500
+++ b/src/HOL/Analysis/document/root.tex Wed Jan 16 19:34:48 2019 -0500
@@ -1,4 +1,4 @@
-\documentclass[11pt,a4paper]{article}
+\documentclass[11pt,a4paper]{book}
\usepackage{graphicx}
\usepackage{isabelle}
\usepackage{isabellesym}