# HG changeset patch
# User wenzelm
# Date 1446469754 -3600
# Node ID b3eb789616c37f533a945f57198b68d5a1b2943b
# Parent  846c72206207de54f789dbef4d1017e4912fb43b
tuned document;

diff -r 846c72206207 -r b3eb789616c3 src/HOL/Isar_Examples/Basic_Logic.thy
--- a/src/HOL/Isar_Examples/Basic_Logic.thy	Mon Nov 02 13:58:19 2015 +0100
+++ b/src/HOL/Isar_Examples/Basic_Logic.thy	Mon Nov 02 14:09:14 2015 +0100
@@ -253,9 +253,7 @@
 proof
   assume "P \<or> P"
   then show P
-  proof                    -- \<open>
-    rule \<open>disjE\<close>: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
-\<close>
+  proof                    -- \<open>rule \<open>disjE\<close>: \smash{$\infer{\<open>C\<close>}{\<open>A \<or> B\<close> & \infer*{\<open>C\<close>}{[\<open>A\<close>]} & \infer*{\<open>C\<close>}{[\<open>B\<close>]}}$}\<close>
     assume P show P by fact
   next
     assume P show P by fact
@@ -324,8 +322,7 @@
 proof
   assume "\<exists>x. P (f x)"
   then show "\<exists>y. P y"
-  proof (rule exE)             --
-    \<open>rule \<open>exE\<close>: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}\<close>
+  proof (rule exE)             -- \<open>rule \<open>exE\<close>: \smash{$\infer{\<open>B\<close>}{\<open>\<exists>x. A(x)\<close> & \infer*{\<open>B\<close>}{[\<open>A(x)\<close>]_x}}$}\<close>
     fix a
     assume "P (f a)" (is "P ?witness")
     then show ?thesis by (rule exI [of P ?witness])
diff -r 846c72206207 -r b3eb789616c3 src/HOL/Isar_Examples/document/root.tex
--- a/src/HOL/Isar_Examples/document/root.tex	Mon Nov 02 13:58:19 2015 +0100
+++ b/src/HOL/Isar_Examples/document/root.tex	Mon Nov 02 14:09:14 2015 +0100
@@ -1,4 +1,15 @@
-\input{style}
+\documentclass[11pt,a4paper]{article}
+\usepackage[only,bigsqcap]{stmaryrd}
+\usepackage{ifthen,proof,amssymb,isabelle,isabellesym}
+\isabellestyle{it}
+\usepackage{pdfsetup}\urlstyle{rm}
+
+\renewcommand{\isacommand}[1]
+{\ifthenelse{\equal{sorry}{#1}}{$\;$\dummyproof}
+  {\ifthenelse{\equal{oops}{#1}}{$\vdots$}{\isakeyword{#1}}}}
+
+\newcommand{\DUMMYPROOF}{{\langle\mathit{proof}\rangle}}
+\newcommand{\dummyproof}{$\DUMMYPROOF$}
 
 \hyphenation{Isabelle}
 
diff -r 846c72206207 -r b3eb789616c3 src/HOL/Isar_Examples/document/style.tex
--- a/src/HOL/Isar_Examples/document/style.tex	Mon Nov 02 13:58:19 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-\documentclass[11pt,a4paper]{article}
-\usepackage[only,bigsqcap]{stmaryrd}
-\usepackage{ifthen,proof,amssymb,isabelle,isabellesym}
-\isabellestyle{it}
-\usepackage{pdfsetup}\urlstyle{rm}
-
-\renewcommand{\isacommand}[1]
-{\ifthenelse{\equal{sorry}{#1}}{$\;$\dummyproof}
-  {\ifthenelse{\equal{oops}{#1}}{$\vdots$}{\isakeyword{#1}}}}
-
-\newcommand{\DUMMYPROOF}{{\langle\idt{proof}\rangle}}
-\newcommand{\dummyproof}{$\DUMMYPROOF$}
-
-\newcommand{\name}[1]{\textsl{#1}}
-
-\newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
-\newcommand{\var}[1]{{?\!\idt{#1}}}
-\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
-\newcommand{\dsh}{\dshsym}
-
-\newcommand{\To}{\to}
-\newcommand{\dt}{{\mathpunct.}}
-\newcommand{\ap}{\mathbin{\!}}
-\newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
-\newcommand{\all}[1]{\forall #1\dt\;}
-\newcommand{\ex}[1]{\exists #1\dt\;}
-\newcommand{\impl}{\to}
-\newcommand{\conj}{\land}
-\newcommand{\disj}{\lor}
-\newcommand{\Impl}{\Longrightarrow}
-
-\newcommand{\Nat}{\mathord{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
-
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: 
diff -r 846c72206207 -r b3eb789616c3 src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Nov 02 13:58:19 2015 +0100
+++ b/src/HOL/ROOT	Mon Nov 02 14:09:14 2015 +0100
@@ -647,7 +647,6 @@
   document_files
     "root.bib"
     "root.tex"
-    "style.tex"
 
 session "HOL-Eisbach" in Eisbach = HOL +
   description {*