# HG changeset patch
# User wenzelm
# Date 1451483726 -3600
# Node ID f55f28132128c9a58afd53918a02e39af8ab8a47
# Parent  3a27957ac658bb7502b717579d231a56b7add45f
proper latex setup;

diff -r 3a27957ac658 -r f55f28132128 src/HOL/Auth/TLS.thy
--- a/src/HOL/Auth/TLS.thy	Wed Dec 30 14:05:51 2015 +0100
+++ b/src/HOL/Auth/TLS.thy	Wed Dec 30 14:55:26 2015 +0100
@@ -170,8 +170,8 @@
           Either party may send its message first.\<close>
 
  | ClientFinished:
-        \<comment>\<open>The occurrence of Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> stops the
-          rule's applying when the Spy has satisfied the "Says A B" by
+        \<comment>\<open>The occurrence of \<open>Notes A \<lbrace>Agent B, Nonce PMS\<rbrace>\<close> stops the
+          rule's applying when the Spy has satisfied the \<open>Says A B\<close> by
           repaying messages sent by the true client; in that case, the
           Spy does not know PMS and could not send ClientFinished.  One
           could simply put @{term "A\<noteq>Spy"} into the rule, but one should not
diff -r 3a27957ac658 -r f55f28132128 src/HOL/Library/document/root.tex
--- a/src/HOL/Library/document/root.tex	Wed Dec 30 14:05:51 2015 +0100
+++ b/src/HOL/Library/document/root.tex	Wed Dec 30 14:55:26 2015 +0100
@@ -2,7 +2,8 @@
 \usepackage{ifthen}
 \usepackage[utf8]{inputenc}
 \usepackage[english]{babel}
-\usepackage{isabelle,isabellesym,amssymb,stmaryrd,textcomp,wasysym}
+\usepackage{amsmath,amssymb,stmaryrd,textcomp,wasysym}
+\usepackage{isabelle,isabellesym}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}
diff -r 3a27957ac658 -r f55f28132128 src/HOL/Multivariate_Analysis/document/root.tex
--- a/src/HOL/Multivariate_Analysis/document/root.tex	Wed Dec 30 14:05:51 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/document/root.tex	Wed Dec 30 14:55:26 2015 +0100
@@ -1,8 +1,6 @@
-
-% HOL/Multivariate_Analysis/document/root.tex
-
 \documentclass[11pt,a4paper]{article}
 \usepackage{graphicx,isabelle,isabellesym,latexsym,textcomp}
+\usepackage{amsmath}
 \usepackage[only,bigsqcap]{stmaryrd}
 \usepackage{pdfsetup}
 
diff -r 3a27957ac658 -r f55f28132128 src/HOL/NSA/document/root.tex
--- a/src/HOL/NSA/document/root.tex	Wed Dec 30 14:05:51 2015 +0100
+++ b/src/HOL/NSA/document/root.tex	Wed Dec 30 14:55:26 2015 +0100
@@ -1,5 +1,6 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{graphicx,isabelle,isabellesym,latexsym,textcomp}
+\usepackage{amsmath}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}
diff -r 3a27957ac658 -r f55f28132128 src/HOL/Probability/document/root.tex
--- a/src/HOL/Probability/document/root.tex	Wed Dec 30 14:05:51 2015 +0100
+++ b/src/HOL/Probability/document/root.tex	Wed Dec 30 14:55:26 2015 +0100
@@ -1,8 +1,6 @@
-
-% HOL/Multivariate_Analysis/document/root.tex
-
 \documentclass[11pt,a4paper]{article}
 \usepackage{graphicx,isabelle,isabellesym,latexsym,textcomp}
+\usepackage{amsmath}
 \usepackage{amssymb}
 \usepackage[only,bigsqcap]{stmaryrd}
 \usepackage[utf8]{inputenc}
diff -r 3a27957ac658 -r f55f28132128 src/HOL/document/root.tex
--- a/src/HOL/document/root.tex	Wed Dec 30 14:05:51 2015 +0100
+++ b/src/HOL/document/root.tex	Wed Dec 30 14:55:26 2015 +0100
@@ -1,6 +1,6 @@
-
 \documentclass[11pt,a4paper]{article}
 \usepackage{graphicx,isabelle,isabellesym,latexsym}
+\usepackage{amsmath}
 \usepackage{amssymb}
 \usepackage{textcomp}
 \usepackage[english]{babel}