--- 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
--- 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}
--- 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}
--- 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}
--- 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}
--- 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}