# HG changeset patch
# User wenzelm
# Date 970605382 -7200
# Node ID e89309dde9d3304eb6ac47bff5c8b368e2343ef0
# Parent  e44b8b7cb01baaa525be34b07418d30764859b2f
tuned;

diff -r e44b8b7cb01b -r e89309dde9d3 src/HOL/Isar_examples/Summation.thy
--- a/src/HOL/Isar_examples/Summation.thy	Tue Oct 03 22:35:44 2000 +0200
+++ b/src/HOL/Isar_examples/Summation.thy	Tue Oct 03 22:36:22 2000 +0200
@@ -60,9 +60,8 @@
   (is "?P n" is "?S n = _")
 proof (induct n)
   show "?P 0" by simp
-
-  fix n
-  have "?S (n + 1) = ?S n + 2 * (n + 1)" by simp
+next
+  fix n have "?S (n + 1) = ?S n + 2 * (n + 1)" by simp
   also assume "?S n = n * (n + 1)"
   also have "... + 2 * (n + 1) = (n + 1) * (n + 2)" by simp
   finally show "?P (Suc n)" by simp
@@ -116,9 +115,8 @@
   (is "?P n" is "?S n = _")
 proof (induct n)
   show "?P 0" by simp
-
-  fix n
-  have "?S (n + 1) = ?S n + 2 * n + 1" by simp
+next
+  fix n have "?S (n + 1) = ?S n + 2 * n + 1" by simp
   also assume "?S n = n^2"
   also have "... + 2 * n + 1 = (n + 1)^2" by simp
   finally show "?P (Suc n)" by simp
@@ -137,9 +135,8 @@
   (is "?P n" is "?S n = _")
 proof (induct n)
   show "?P 0" by simp
-
-  fix n
-  have "?S (n + 1) = ?S n + #6 * (n + 1)^2" by (simp add: distrib)
+next
+  fix n have "?S (n + 1) = ?S n + #6 * (n + 1)^2" by (simp add: distrib)
   also assume "?S n = n * (n + 1) * (2 * n + 1)"
   also have "... + #6 * (n + 1)^2 =
     (n + 1) * (n + 2) * (2 * (n + 1) + 1)" by (simp add: distrib)
@@ -151,9 +148,8 @@
   (is "?P n" is "?S n = _")
 proof (induct n)
   show "?P 0" by (simp add: power_eq_if)
-
-  fix n
-  have "?S (n + 1) = ?S n + #4 * (n + 1)^#3"
+next
+  fix n have "?S (n + 1) = ?S n + #4 * (n + 1)^#3"
     by (simp add: power_eq_if distrib)
   also assume "?S n = (n * (n + 1))^2"
   also have "... + #4 * (n + 1)^#3 = ((n + 1) * ((n + 1) + 1))^2"
diff -r e44b8b7cb01b -r e89309dde9d3 src/HOL/Isar_examples/W_correct.thy
--- a/src/HOL/Isar_examples/W_correct.thy	Tue Oct 03 22:35:44 2000 +0200
+++ b/src/HOL/Isar_examples/W_correct.thy	Tue Oct 03 22:36:22 2000 +0200
@@ -10,7 +10,7 @@
 theory W_correct = Main + Type:
 
 text_raw {*
-  \footnote{Based upon \url{http://isabelle.in.tum.de/library/HOL/W0}
+  \footnote{Based upon \url{http://isabelle.in.tum.de/library/HOL/W0/}
   by Dieter Nazareth and Tobias Nipkow.}
 *}
 
@@ -30,7 +30,7 @@
   "_has_type" :: "[typ list, expr, typ] => bool"
     ("((_) |-/ (_) :: (_))" [60, 0, 60] 60)
 translations
-  "a |- e :: t" == "(a,e,t) : has_type"
+  "a |- e :: t" == "(a, e, t) : has_type"
 
 inductive has_type
   intros [simp]
diff -r e44b8b7cb01b -r e89309dde9d3 src/HOL/Isar_examples/document/root.tex
--- a/src/HOL/Isar_examples/document/root.tex	Tue Oct 03 22:35:44 2000 +0200
+++ b/src/HOL/Isar_examples/document/root.tex	Tue Oct 03 22:36:22 2000 +0200
@@ -23,19 +23,27 @@
 
 \parindent 0pt \parskip 0.5ex
 
-\input{BasicLogic}
-\input{Cantor}
-\input{Peirce}
-\input{ExprCompiler}
-\input{Group}
-\input{Summation}
-\input{KnasterTarski}
-\input{MutilatedCheckerboard}
-\input{MultisetOrder}
-\input{W_correct}
-\input{Fibonacci}
-\input{Puzzle}
-\input{NestedDatatype}
+\input{BasicLogic.tex}
+\input{Cantor.tex}
+\input{Peirce.tex}
+\input{ExprCompiler.tex}
+\input{Group.tex}
+\input{Summation.tex}
+\input{KnasterTarski.tex}
+\input{MutilatedCheckerboard.tex}
+%\input{Multiset0.tex}
+%\input{Acc.tex}
+%\input{Multiset.tex}
+\input{MultisetOrder.tex}
+%\input{Maybe.tex}
+%\input{Type.tex}
+\input{W_correct.tex}
+%\input{Primes.tex}
+\input{Fibonacci.tex}
+\input{Puzzle.tex}
+\input{NestedDatatype.tex}
+\input{Hoare.tex}
+\input{HoareEx.tex}
 
 \nocite{isabelle-isar-ref,Wenzel:1999:TPHOL}
 \bibliographystyle{plain}
diff -r e44b8b7cb01b -r e89309dde9d3 src/HOL/Isar_examples/document/style.tex
--- a/src/HOL/Isar_examples/document/style.tex	Tue Oct 03 22:35:44 2000 +0200
+++ b/src/HOL/Isar_examples/document/style.tex	Tue Oct 03 22:36:22 2000 +0200
@@ -2,11 +2,18 @@
 %% $Id$
 
 \documentclass[11pt,a4paper]{article}
-\usepackage{proof,isabelle,isabellesym,pdfsetup}
-\urlstyle{rm}
+\usepackage{ifthen,proof,isabelle,isabellesym}
+\usepackage{pdfsetup}\urlstyle{rm}
 
 \renewcommand{\isamarkupheader}[1]{\section{#1}}
 
+\renewcommand{\isacommand}[1]
+{\ifthenelse{\equal{sorry}{#1}}{$\;$\dummyproof}
+  {\ifthenelse{\equal{oops}{#1}}{$\vdots$}{\isakeyword{#1}}}}
+
+\newcommand{\DUMMYPROOF}{{\langle\idt{proof}\rangle}}
+\newcommand{\dummyproof}{$\DUMMYPROOF$}
+
 \newcommand{\name}[1]{\textsl{#1}}
 
 \newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}