--- a/src/Doc/ROOT Wed Dec 06 09:11:27 2017 +0100
+++ b/src/Doc/ROOT Wed Dec 06 15:17:05 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 09:11:27 2017 +0100
+++ b/src/HOL/Analysis/L2_Norm.thy Wed Dec 06 15:17:05 2017 +0100
@@ -2,13 +2,13 @@
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
begin
-definition
+definition %important
"setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
lemma setL2_cong:
@@ -74,9 +74,9 @@
unfolding setL2_def
by (simp add: sum_nonneg sum_nonneg_eq_0_iff)
-lemma setL2_triangle_ineq:
+lemma %important setL2_triangle_ineq:
shows "setL2 (\<lambda>i. f i + g i) A \<le> setL2 f A + setL2 g A"
-proof (cases "finite A")
+proof %unimportant (cases "finite A")
case False
thus ?thesis by simp
next
--- a/src/HOL/Analysis/document/root.tex Wed Dec 06 09:11:27 2017 +0100
+++ b/src/HOL/Analysis/document/root.tex Wed Dec 06 15:17:05 2017 +0100
@@ -15,7 +15,7 @@
\begin{document}
-\title{Multivariate Analysis}
+\title{Analysis}
\maketitle
\tableofcontents