1.1 --- a/src/HOL/CTL/CTL.thy	Sun Oct 21 19:41:43 2001 +0200
     1.2 +++ b/src/HOL/CTL/CTL.thy	Sun Oct 21 19:42:24 2001 +0200
     1.3 @@ -4,8 +4,8 @@
     1.4  section {* CTL formulae *}
     1.5  
     1.6  text {*
     1.7 -  \tweakskip We formalize basic concepts of Computational Tree Logic
     1.8 -  (CTL) \cite{McMillan-PhDThesis,McMillan-LectureNotes} within the
     1.9 +  We formalize basic concepts of Computational Tree Logic (CTL)
    1.10 +  \cite{McMillan-PhDThesis,McMillan-LectureNotes} within the
    1.11    simply-typed set theory of HOL.
    1.12  
    1.13    By using the common technique of ``shallow embedding'', a CTL
    1.14 @@ -74,8 +74,7 @@
    1.15  section {* Basic fixed point properties *}
    1.16  
    1.17  text {*
    1.18 -  \tweakskip First of all, we use the de-Morgan property of fixed
    1.19 -  points
    1.20 +  First of all, we use the de-Morgan property of fixed points
    1.21  *}
    1.22  
    1.23  lemma lfp_gfp: "lfp f = - gfp (\<lambda>s . - (f (- s)))"
    1.24 @@ -183,10 +182,10 @@
    1.25  section {* The tree induction principle \label{sec:calc-ctl-tree-induct} *}
    1.26  
    1.27  text {*
    1.28 -  \tweakskip With the most basic facts available, we are now able to
    1.29 -  establish a few more interesting results, leading to the \emph{tree
    1.30 -  induction} principle for @{text AG} (see below).  We will use some
    1.31 -  elementary monotonicity and distributivity rules.
    1.32 +  With the most basic facts available, we are now able to establish a
    1.33 +  few more interesting results, leading to the \emph{tree induction}
    1.34 +  principle for @{text AG} (see below).  We will use some elementary
    1.35 +  monotonicity and distributivity rules.
    1.36  *}
    1.37  
    1.38  lemma AX_int: "\<AX> (p \<inter> q) = \<AX> p \<inter> \<AX> q" by auto 
    1.39 @@ -279,7 +278,7 @@
    1.40  section {* An application of tree induction \label{sec:calc-ctl-commute} *}
    1.41  
    1.42  text {*
    1.43 -  \tweakskip Further interesting properties of CTL expressions may be
    1.44 +  Further interesting properties of CTL expressions may be
    1.45    demonstrated with the help of tree induction; here we show that
    1.46    @{text \<AX>} and @{text \<AG>} commute.
    1.47  *}

     2.1 --- a/src/HOL/CTL/document/root.tex	Sun Oct 21 19:41:43 2001 +0200
     2.2 +++ b/src/HOL/CTL/document/root.tex	Sun Oct 21 19:42:24 2001 +0200
     2.3 @@ -23,7 +23,6 @@
     2.4  \bigskip
     2.5  
     2.6  \parindent 0pt\parskip 0.5ex
     2.7 -\newcommand{\tweakskip}{\vspace{-\smallskipamount}\vspace{-\parskip}}
     2.8  
     2.9  \input{session}
    2.10  

     3.1 --- a/src/HOL/Unix/document/root.tex	Sun Oct 21 19:41:43 2001 +0200
     3.2 +++ b/src/HOL/Unix/document/root.tex	Sun Oct 21 19:42:24 2001 +0200
     3.3 @@ -6,7 +6,6 @@
     3.4  \urlstyle{rm}
     3.5  \isabellestyle{it}
     3.6  
     3.7 -\renewcommand{\isabeginpar}{\par\smallskip}
     3.8  \renewcommand{\isamarkupcmt}[1]{{\isastylecmt---~~#1}}
     3.9  
    3.10  \newcommand{\secref}[1]{\S\ref{#1}}