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