# HG changeset patch
# User wenzelm
# Date 1003686144 -7200
# Node ID 03801fd2f8fcdd7cb3ccd780d99df5984c9848f5
# Parent  38d8075ebff66e1c65a6414bcf6f83abe7c0779f
improved spacing;

diff -r 38d8075ebff6 -r 03801fd2f8fc src/HOL/CTL/CTL.thy
--- a/src/HOL/CTL/CTL.thy	Sun Oct 21 19:41:43 2001 +0200
+++ b/src/HOL/CTL/CTL.thy	Sun Oct 21 19:42:24 2001 +0200
@@ -4,8 +4,8 @@
 section {* CTL formulae *}
 
 text {*
-  \tweakskip We formalize basic concepts of Computational Tree Logic
-  (CTL) \cite{McMillan-PhDThesis,McMillan-LectureNotes} within the
+  We formalize basic concepts of Computational Tree Logic (CTL)
+  \cite{McMillan-PhDThesis,McMillan-LectureNotes} within the
   simply-typed set theory of HOL.
 
   By using the common technique of ``shallow embedding'', a CTL
@@ -74,8 +74,7 @@
 section {* Basic fixed point properties *}
 
 text {*
-  \tweakskip First of all, we use the de-Morgan property of fixed
-  points
+  First of all, we use the de-Morgan property of fixed points
 *}
 
 lemma lfp_gfp: "lfp f = - gfp (\<lambda>s . - (f (- s)))"
@@ -183,10 +182,10 @@
 section {* The tree induction principle \label{sec:calc-ctl-tree-induct} *}
 
 text {*
-  \tweakskip With the most basic facts available, we are now able to
-  establish a few more interesting results, leading to the \emph{tree
-  induction} principle for @{text AG} (see below).  We will use some
-  elementary monotonicity and distributivity rules.
+  With the most basic facts available, we are now able to establish a
+  few more interesting results, leading to the \emph{tree induction}
+  principle for @{text AG} (see below).  We will use some elementary
+  monotonicity and distributivity rules.
 *}
 
 lemma AX_int: "\<AX> (p \<inter> q) = \<AX> p \<inter> \<AX> q" by auto 
@@ -279,7 +278,7 @@
 section {* An application of tree induction \label{sec:calc-ctl-commute} *}
 
 text {*
-  \tweakskip Further interesting properties of CTL expressions may be
+  Further interesting properties of CTL expressions may be
   demonstrated with the help of tree induction; here we show that
   @{text \<AX>} and @{text \<AG>} commute.
 *}
diff -r 38d8075ebff6 -r 03801fd2f8fc src/HOL/CTL/document/root.tex
--- a/src/HOL/CTL/document/root.tex	Sun Oct 21 19:41:43 2001 +0200
+++ b/src/HOL/CTL/document/root.tex	Sun Oct 21 19:42:24 2001 +0200
@@ -23,7 +23,6 @@
 \bigskip
 
 \parindent 0pt\parskip 0.5ex
-\newcommand{\tweakskip}{\vspace{-\smallskipamount}\vspace{-\parskip}}
 
 \input{session}
 
diff -r 38d8075ebff6 -r 03801fd2f8fc src/HOL/Unix/document/root.tex
--- a/src/HOL/Unix/document/root.tex	Sun Oct 21 19:41:43 2001 +0200
+++ b/src/HOL/Unix/document/root.tex	Sun Oct 21 19:42:24 2001 +0200
@@ -6,7 +6,6 @@
 \urlstyle{rm}
 \isabellestyle{it}
 
-\renewcommand{\isabeginpar}{\par\smallskip}
 \renewcommand{\isamarkupcmt}[1]{{\isastylecmt---~~#1}}
 
 \newcommand{\secref}[1]{\S\ref{#1}}