# HG changeset patch
# User immler
# Date 1547685288 18000
# Node ID 56acd449da41acb13ce5e71ea4f01dbe037c2077
# Parent  880ab0f27ddf62cd666a9f557274b6ab32282968
chapters for analysis manual

diff -r 880ab0f27ddf -r 56acd449da41 src/HOL/Analysis/Analysis.thy
--- 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
diff -r 880ab0f27ddf -r 56acd449da41 src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- 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"
diff -r 880ab0f27ddf -r 56acd449da41 src/HOL/Analysis/Elementary_Topology.thy
--- 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)"
diff -r 880ab0f27ddf -r 56acd449da41 src/HOL/Analysis/L2_Norm.thy
--- 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)"
 
diff -r 880ab0f27ddf -r 56acd449da41 src/HOL/Analysis/Sigma_Algebra.thy
--- 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,
diff -r 880ab0f27ddf -r 56acd449da41 src/HOL/Analysis/Starlike.thy
--- 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"
diff -r 880ab0f27ddf -r 56acd449da41 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- 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"
diff -r 880ab0f27ddf -r 56acd449da41 src/HOL/Analysis/document/root.tex
--- 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}