author wenzelm Tue, 03 Oct 2000 22:36:22 +0200 changeset 10146 e89309dde9d3 parent 10145 e44b8b7cb01b child 10147 178deaacb244
tuned;
--- 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"
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}

+{\ifthenelse{\equal{sorry}{#1}}{$\;$\dummyproof}
+  {\ifthenelse{\equal{oops}{#1}}{$\vdots$}{\isakeyword{#1}}}}
+\newcommand{\dummyproof}{$\DUMMYPROOF$}