--- a/src/Doc/ROOT Wed Dec 06 20:43:09 2017 +0100
+++ b/src/Doc/ROOT Wed Dec 06 21:01:01 2017 +0100
@@ -1,5 +1,19 @@
chapter Doc
+session Analysis (doc) in "../HOL/Analysis" = HOL +
+ options [document_variants = "analysis",
+ (*skip_proofs = true,*) quick_and_dirty,
+ document = pdf, document_output = "output",
+ document_variants = "document=-proof,-ML,+important,-unimportant",
+ document_tags = "unimportant"]
+ sessions
+ "HOL-Library"
+ "HOL-Computational_Algebra"
+ theories
+ Analysis
+ document_files
+ "root.tex"
+
session Classes (doc) in "Classes" = HOL +
options [document_variants = "classes", quick_and_dirty]
theories [document = false] Setup
--- a/src/HOL/Analysis/L2_Norm.thy Wed Dec 06 20:43:09 2017 +0100
+++ b/src/HOL/Analysis/L2_Norm.thy Wed Dec 06 21:01:01 2017 +0100
@@ -2,7 +2,7 @@
Author: Brian Huffman, Portland State University
*)
-section \<open>Square root of sum of squares\<close>
+section \<open>L2 Norm\<close>
theory L2_Norm
imports Complex_Main
--- a/src/HOL/Analysis/document/root.tex Wed Dec 06 20:43:09 2017 +0100
+++ b/src/HOL/Analysis/document/root.tex Wed Dec 06 21:01:01 2017 +0100
@@ -15,7 +15,7 @@
\begin{document}
-\title{Multivariate Analysis}
+\title{Analysis}
\maketitle
\tableofcontents