# HG changeset patch
# User huffman
# Date 1272141112 25200
# Node ID 068a01b4bc56a83e63160f2b583dd5fd44e08dde
# Parent  82356c9e218abb7f271cd9b5b8c880bbed78eb70
document generation for Multivariate_Analysis

diff -r 82356c9e218a -r 068a01b4bc56 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sat Apr 24 11:11:09 2010 -0700
+++ b/src/HOL/IsaMakefile	Sat Apr 24 13:31:52 2010 -0700
@@ -1079,6 +1079,7 @@
 
 $(OUT)/HOL-Multivariate_Analysis: $(OUT)/HOL-SMT	\
   Multivariate_Analysis/ROOT.ML				\
+  Multivariate_Analysis/document/root.tex		\
   Multivariate_Analysis/L2_Norm.thy			\
   Multivariate_Analysis/Multivariate_Analysis.thy	\
   Multivariate_Analysis/Determinants.thy		\
diff -r 82356c9e218a -r 068a01b4bc56 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sat Apr 24 11:11:09 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sat Apr 24 13:31:52 2010 -0700
@@ -1350,7 +1350,7 @@
   using assms by auto
 
 text {*Still more general form; could derive this directly without using the 
-  rather involved HOMEOMORPHIC_CONVEX_COMPACT theorem, just using
+  rather involved @{text "HOMEOMORPHIC_CONVEX_COMPACT"} theorem, just using
   a scaling and translation to put the set inside the unit cube. *}
 
 lemma brouwer: fixes f::"real^'n \<Rightarrow> real^'n"
diff -r 82356c9e218a -r 068a01b4bc56 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Sat Apr 24 11:11:09 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Sat Apr 24 13:31:52 2010 -0700
@@ -91,7 +91,7 @@
   "a \<in> s \<Longrightarrow> open s \<Longrightarrow> ((f has_derivative f') (at a within s) \<longleftrightarrow> (f has_derivative f') (at a))"
   unfolding has_derivative_within has_derivative_at using Lim_within_open by auto
 
-subsection {* Derivatives on real = Derivatives on real^1 *}
+subsection {* Derivatives on real = Derivatives on @{typ "real^1"} *}
 
 lemma dist_vec1_0[simp]: "dist(vec1 (x::real)) 0 = norm x" unfolding vector_dist_norm by(auto simp add:vec1_dest_vec1_simps)
 
@@ -626,7 +626,7 @@
     unfolding abs_mult diff_minus_eq_add scaleR.minus_left unfolding group_simps by (auto intro: mult_pos_pos)
 qed
 
-subsection {* In particular if we have a mapping into R^1. *}
+subsection {* In particular if we have a mapping into @{typ "real^1"}. *}
 
 lemma differential_zero_maxmin: fixes f::"real^'a \<Rightarrow> real"
   assumes "x \<in> s" "open s" "(f has_derivative f') (at x)"
@@ -1212,7 +1212,7 @@
   shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x)"
   using has_derivative_bilinear_within[of f f' x UNIV g g' h] unfolding within_UNIV using assms by auto
 
-subsection {* Considering derivative R(^1)->R^n as a vector. *}
+subsection {* Considering derivative @{typ "real^1 \<Rightarrow> real^'n"} as a vector. *}
 
 definition has_vector_derivative :: "(real \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> ('b) \<Rightarrow> (real net \<Rightarrow> bool)"
 (infixl "has'_vector'_derivative" 12) where
diff -r 82356c9e218a -r 068a01b4bc56 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sat Apr 24 11:11:09 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sat Apr 24 13:31:52 2010 -0700
@@ -114,7 +114,7 @@
   instance by (intro_classes)
 end
 
-text{* The ordering on real^1 is linear. *}
+text{* The ordering on @{typ "real^1"} is linear. *}
 
 class cart_one = assumes UNIV_one: "card (UNIV \<Colon> 'a set) = Suc 0"
 begin
diff -r 82356c9e218a -r 068a01b4bc56 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Sat Apr 24 11:11:09 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Sat Apr 24 13:31:52 2010 -0700
@@ -2181,7 +2181,7 @@
   unfolding operative_tagged_division[OF monoidal_monoid operative_content assms,THEN sym]
   apply(subst setsum_iterate) using assms by auto
 
-subsection {* Finally, the integral of a constant\<forall> *}
+subsection {* Finally, the integral of a constant *}
 
 lemma has_integral_const[intro]:
   "((\<lambda>x. c) has_integral (content({a..b::real^'n}) *\<^sub>R c)) ({a..b})"
diff -r 82356c9e218a -r 068a01b4bc56 src/HOL/Multivariate_Analysis/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Multivariate_Analysis/document/root.tex	Sat Apr 24 13:31:52 2010 -0700
@@ -0,0 +1,31 @@
+
+% HOL/Multivariate_Analysis/document/root.tex
+
+\documentclass[11pt,a4paper]{article}
+\usepackage{graphicx,isabelle,isabellesym,latexsym}
+\usepackage[only,bigsqcap]{stmaryrd}
+\usepackage[latin1]{inputenc}
+\usepackage{pdfsetup}
+
+\urlstyle{rm}
+\isabellestyle{it}
+\pagestyle{myheadings}
+
+\begin{document}
+
+\title{Multivariate Analysis}
+\maketitle
+
+\tableofcontents
+
+\begin{center}
+  \includegraphics[scale=0.45]{session_graph}
+\end{center}
+
+\renewcommand{\isamarkupheader}[1]%
+{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
+
+\parindent 0pt\parskip 0.5ex
+\input{session}
+
+\end{document}