--- a/src/HOL/Isar_examples/MultisetOrder.thy Sun Mar 26 20:13:53 2000 +0200
+++ b/src/HOL/Isar_examples/MultisetOrder.thy Sun Mar 26 20:16:34 2000 +0200
@@ -12,11 +12,10 @@
text_raw {*
\footnote{Original tactic script by Tobias Nipkow (see
\url{http://isabelle.in.tum.de/library/HOL/Induct/Multiset.html}),
- based on a pen-and-paper proof due to Wilfried Buchholz.}
+ based on a pen-and-paper proof due to Wilfried Buchholz.}\isanewline
*};
(* FIXME move? *)
-
theorems [induct type: multiset] = multiset_induct;
theorems [induct set: wf] = wf_induct;
theorems [induct set: acc] = acc_induct;
--- a/src/HOL/Isar_examples/Summation.thy Sun Mar 26 20:13:53 2000 +0200
+++ b/src/HOL/Isar_examples/Summation.thy Sun Mar 26 20:16:34 2000 +0200
@@ -44,12 +44,10 @@
"_SUM" :: "[idt, nat, nat] => nat"
("SUM _ < _. _" [0, 0, 10] 10);
translations
- "SUM i < k. b" == "sum (\<lambda>i. b) k";
+ "SUM i < k. b" == "sum (\\<lambda>i. b) k";
-subsection {* Summation laws *};
-
-text_raw {* \begin{comment} *};
+subsection {* Summation laws *}; (*<*)
(* FIXME binary arithmetic does not yet work here *)
@@ -65,7 +63,7 @@
theorems [simp] = add_mult_distrib add_mult_distrib2 mult_ac;
-text_raw {* \end{comment} *};
+(*>*)
text {*
The sum of natural numbers $0 + \cdots + n$ equals $n \times (n +
--- a/src/HOL/Isar_examples/document/style.tex Sun Mar 26 20:13:53 2000 +0200
+++ b/src/HOL/Isar_examples/document/style.tex Sun Mar 26 20:16:34 2000 +0200
@@ -2,7 +2,7 @@
%% $Id$
\documentclass[11pt,a4paper]{article}
-\usepackage{comment,proof,isabelle,isabellesym,pdfsetup}
+\usepackage{proof,isabelle,isabellesym,pdfsetup}
\renewcommand{\isamarkupheader}[1]{\section{#1}}