author wenzelm Sun, 21 Oct 2001 19:42:24 +0200 changeset 11862 03801fd2f8fc parent 11861 38d8075ebff6 child 11863 87643169ae7d
improved spacing;
 src/HOL/CTL/CTL.thy file | annotate | diff | comparison | revisions src/HOL/CTL/document/root.tex file | annotate | diff | comparison | revisions src/HOL/Unix/document/root.tex file | annotate | diff | comparison | revisions
--- 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.
*}
--- 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}

--- 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}}