tuned document;
authorwenzelm
Mon Nov 02 14:09:14 2015 +0100 (2015-11-02)
changeset 61542b3eb789616c3
parent 61541 846c72206207
child 61543 de44d4fa5ef0
tuned document;
src/HOL/Isar_Examples/Basic_Logic.thy
src/HOL/Isar_Examples/document/root.tex
src/HOL/Isar_Examples/document/style.tex
src/HOL/ROOT
     1.1 --- a/src/HOL/Isar_Examples/Basic_Logic.thy	Mon Nov 02 13:58:19 2015 +0100
     1.2 +++ b/src/HOL/Isar_Examples/Basic_Logic.thy	Mon Nov 02 14:09:14 2015 +0100
     1.3 @@ -253,9 +253,7 @@
     1.4  proof
     1.5    assume "P \<or> P"
     1.6    then show P
     1.7 -  proof                    -- \<open>
     1.8 -    rule \<open>disjE\<close>: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
     1.9 -\<close>
    1.10 +  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>
    1.11      assume P show P by fact
    1.12    next
    1.13      assume P show P by fact
    1.14 @@ -324,8 +322,7 @@
    1.15  proof
    1.16    assume "\<exists>x. P (f x)"
    1.17    then show "\<exists>y. P y"
    1.18 -  proof (rule exE)             --
    1.19 -    \<open>rule \<open>exE\<close>: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}\<close>
    1.20 +  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>
    1.21      fix a
    1.22      assume "P (f a)" (is "P ?witness")
    1.23      then show ?thesis by (rule exI [of P ?witness])
     2.1 --- a/src/HOL/Isar_Examples/document/root.tex	Mon Nov 02 13:58:19 2015 +0100
     2.2 +++ b/src/HOL/Isar_Examples/document/root.tex	Mon Nov 02 14:09:14 2015 +0100
     2.3 @@ -1,4 +1,15 @@
     2.4 -\input{style}
     2.5 +\documentclass[11pt,a4paper]{article}
     2.6 +\usepackage[only,bigsqcap]{stmaryrd}
     2.7 +\usepackage{ifthen,proof,amssymb,isabelle,isabellesym}
     2.8 +\isabellestyle{it}
     2.9 +\usepackage{pdfsetup}\urlstyle{rm}
    2.10 +
    2.11 +\renewcommand{\isacommand}[1]
    2.12 +{\ifthenelse{\equal{sorry}{#1}}{$\;$\dummyproof}
    2.13 +  {\ifthenelse{\equal{oops}{#1}}{$\vdots$}{\isakeyword{#1}}}}
    2.14 +
    2.15 +\newcommand{\DUMMYPROOF}{{\langle\mathit{proof}\rangle}}
    2.16 +\newcommand{\dummyproof}{$\DUMMYPROOF$}
    2.17  
    2.18  \hyphenation{Isabelle}
    2.19  
     3.1 --- a/src/HOL/Isar_Examples/document/style.tex	Mon Nov 02 13:58:19 2015 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,38 +0,0 @@
     3.4 -\documentclass[11pt,a4paper]{article}
     3.5 -\usepackage[only,bigsqcap]{stmaryrd}
     3.6 -\usepackage{ifthen,proof,amssymb,isabelle,isabellesym}
     3.7 -\isabellestyle{it}
     3.8 -\usepackage{pdfsetup}\urlstyle{rm}
     3.9 -
    3.10 -\renewcommand{\isacommand}[1]
    3.11 -{\ifthenelse{\equal{sorry}{#1}}{$\;$\dummyproof}
    3.12 -  {\ifthenelse{\equal{oops}{#1}}{$\vdots$}{\isakeyword{#1}}}}
    3.13 -
    3.14 -\newcommand{\DUMMYPROOF}{{\langle\idt{proof}\rangle}}
    3.15 -\newcommand{\dummyproof}{$\DUMMYPROOF$}
    3.16 -
    3.17 -\newcommand{\name}[1]{\textsl{#1}}
    3.18 -
    3.19 -\newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
    3.20 -\newcommand{\var}[1]{{?\!\idt{#1}}}
    3.21 -\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
    3.22 -\newcommand{\dsh}{\dshsym}
    3.23 -
    3.24 -\newcommand{\To}{\to}
    3.25 -\newcommand{\dt}{{\mathpunct.}}
    3.26 -\newcommand{\ap}{\mathbin{\!}}
    3.27 -\newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
    3.28 -\newcommand{\all}[1]{\forall #1\dt\;}
    3.29 -\newcommand{\ex}[1]{\exists #1\dt\;}
    3.30 -\newcommand{\impl}{\to}
    3.31 -\newcommand{\conj}{\land}
    3.32 -\newcommand{\disj}{\lor}
    3.33 -\newcommand{\Impl}{\Longrightarrow}
    3.34 -
    3.35 -\newcommand{\Nat}{\mathord{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
    3.36 -
    3.37 -
    3.38 -%%% Local Variables: 
    3.39 -%%% mode: latex
    3.40 -%%% TeX-master: "root"
    3.41 -%%% End: 
     4.1 --- a/src/HOL/ROOT	Mon Nov 02 13:58:19 2015 +0100
     4.2 +++ b/src/HOL/ROOT	Mon Nov 02 14:09:14 2015 +0100
     4.3 @@ -647,7 +647,6 @@
     4.4    document_files
     4.5      "root.bib"
     4.6      "root.tex"
     4.7 -    "style.tex"
     4.8  
     4.9  session "HOL-Eisbach" in Eisbach = HOL +
    4.10    description {*