# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1320682406 0
# Node ID 1343540ed715ae7e0028dc1a8ffb3131c7f7c579
# Parent  780100cd40609495190aba548e5661576be9adbf
tuned

diff -r 780100cd4060 -r 1343540ed715 ProgTutorial/First_Steps.thy
--- a/ProgTutorial/First_Steps.thy	Mon Nov 07 13:36:07 2011 +0000
+++ b/ProgTutorial/First_Steps.thy	Mon Nov 07 16:13:26 2011 +0000
@@ -13,15 +13,10 @@
 chapter {* First Steps\label{chp:firststeps} *}
 
 text {*
-   \begin{flushright}
-  {\em
-  ``We will most likely never realize the full importance of painting the Tower,\\ 
-  that it is the essential element in the conservation of metal works and the\\ 
-  more meticulous the paint job, the longer the tower shall endure.''} \\[1ex]
-  Gustave Eiffel, in his book {\em The 300-Meter Tower}.\footnote{The Eiffel Tower has been 
-  re-painted 18 times since its initial construction, an average of once every 
-  seven years. It takes more than one year for a team of 25 painters to paint the tower 
-  from top to bottom.}
+  \begin{flushright}
+  {\em ``The most effective debugging tool is still careful thought,\\ 
+  coupled with judiciously placed print statements.''} \\[1ex]
+  Brian Kernighan, in {\em Unix for Beginners}, 1979
   \end{flushright}
 
   \medskip
diff -r 780100cd4060 -r 1343540ed715 ProgTutorial/Package/Ind_Intro.thy
--- a/ProgTutorial/Package/Ind_Intro.thy	Mon Nov 07 13:36:07 2011 +0000
+++ b/ProgTutorial/Package/Ind_Intro.thy	Mon Nov 07 16:13:26 2011 +0000
@@ -13,6 +13,18 @@
 chapter {* How to Write a Definitional Package\label{chp:package} *}
 
 text {*
+   \begin{flushright}
+  {\em
+  ``We will most likely never realize the full importance of painting the Tower,\\ 
+  that it is the essential element in the conservation of metal works and the\\ 
+  more meticulous the paint job, the longer the tower shall endure.''} \\[1ex]
+  Gustave Eiffel, in his book {\em The 300-Meter Tower}.\footnote{The Eiffel Tower has been 
+  re-painted 18 times since its initial construction, an average of once every 
+  seven years. It takes more than one year for a team of 25 painters to paint the tower 
+  from top to bottom.}
+  \end{flushright}
+
+  \medskip
   HOL is based on just a few primitive constants, like equality and
   implication, whose properties are described by axioms. All other concepts,
   such as inductive predicates, datatypes or recursive functions, are defined
diff -r 780100cd4060 -r 1343540ed715 ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Mon Nov 07 13:36:07 2011 +0000
+++ b/ProgTutorial/Tactical.thy	Mon Nov 07 16:13:26 2011 +0000
@@ -13,13 +13,6 @@
 chapter {* Tactical Reasoning\label{chp:tactical} *}
 
 text {*
-   \begin{flushright}
-  {\em ``The most effective debugging tool is still careful thought,\\ 
-  coupled with judiciously placed print statements.''} \\[1ex]
-  Brian Kernighan, in {\em Unix for Beginners}, 1979
-  \end{flushright}
-
-  \medskip
   One of the main reason for descending to the ML-level of Isabelle is to be
   able to implement automatic proof procedures. Such proof procedures can
   considerably lessen the burden of manual reasoning. They are centred around
diff -r 780100cd4060 -r 1343540ed715 progtutorial.pdf
Binary file progtutorial.pdf has changed