# HG changeset patch
# User nipkow
# Date 1031585309 -7200
# Node ID 5b71e1408ac451749558b26a886af20b6c840695
# Parent  daefa3ac893376d8f5e52434751f455b92a818ca
*** empty log message ***

diff -r daefa3ac8933 -r 5b71e1408ac4 doc-src/TutorialI/IsarOverview/Isar/Calc.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/IsarOverview/Isar/Calc.thy	Mon Sep 09 17:28:29 2002 +0200
@@ -0,0 +1,30 @@
+theory Calc = Main:
+
+axclass
+  group < zero, plus, minus
+  assoc:       "(x + y) + z = x + (y + z)"
+  left_0:      "0 + x = x"
+  left_minus:  "-x + x = 0"
+
+theorem right_minus: "x + -x = (0::'a::group)"
+proof -
+  have   "x + -x = (-(-x) + -x) + (x + -x)"
+    by (simp only: left_0 left_minus)
+  also have "... = -(-x) + ((-x + x) + -x)"
+    by (simp only: group.assoc)
+  also have "... = 0"
+    by (simp only: left_0 left_minus)
+  finally show ?thesis .
+qed
+
+
+lemma assumes R: "(a,b) \<in> R" "(b,c) \<in> R" "(c,d) \<in> R"
+      shows "(a,d) \<in> R\<^sup>*"
+proof -
+       have "(a,b) \<in> R\<^sup>*" ..
+  also have "(b,c) \<in> R\<^sup>*" ..
+  also have "(c,d) \<in> R\<^sup>*" ..
+  finally show ?thesis .
+qed
+
+end
\ No newline at end of file
diff -r daefa3ac8933 -r 5b71e1408ac4 doc-src/TutorialI/Overview/Slides/main.tex
--- a/doc-src/TutorialI/Overview/Slides/main.tex	Mon Sep 09 17:07:12 2002 +0200
+++ b/doc-src/TutorialI/Overview/Slides/main.tex	Mon Sep 09 17:28:29 2002 +0200
@@ -113,6 +113,7 @@
 \end{itemize}
 \end{cslide}
 %-----------------------------------------------------------------------------
+\overlays{2}{
 \begin{cslide}{Functional Programming}
 \begin{itemize}
 \item An introductory example
@@ -121,7 +122,12 @@
 \item Advanced datatypes
 \item Advanced recursive functions
 \end{itemize}
-\end{cslide}
+\FromSlide{2}
+There is more:\\
+\emph{\blue records},
+\emph{\blue (axiomatic) type classes},
+\emph{\blue program extraction}, \dots!
+\end{cslide}}
 %-----------------------------------------------------------------------------
 \begin{cslide}{Logic (Natural Deduction)}
 \begin{itemize}
@@ -170,7 +176,7 @@
 \quad\textbf{have} {\blue\sl intermediate result} \textbf{by} ...\\
 \quad\vdots\\
 \quad\textbf{have} {\blue\sl intermediate result} \textbf{by} ...\\
-\quad\textbf{show} {\blue\sl conclusion}\\
+\quad\textbf{show} {\blue\sl conclusion} \textbf{by} ...\\
 \textbf{qed}
 \end{tabular}
 \bigskip
@@ -197,6 +203,7 @@
 \begin{itemize}
 \item Logic
 \item Induction
+\item Calculation
 \end{itemize}
 \end{cslide}
 %-----------------------------------------------------------------------------