--- 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])
--- 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}
--- 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:
--- 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 {*