# HG changeset patch
# User nipkow
# Date 1512569825 -3600
# Node ID db609ac2c3073683b06fdf03aff96dd5f391c622
# Parent  fa1173288322a146f659d513bf5e752fc25a6d6a
initial version of Analysis document

diff -r fa1173288322 -r db609ac2c307 src/Doc/ROOT
--- 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
diff -r fa1173288322 -r db609ac2c307 src/HOL/Analysis/L2_Norm.thy
--- 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
diff -r fa1173288322 -r db609ac2c307 src/HOL/Analysis/document/root.tex
--- 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