# HG changeset patch
# User wenzelm
# Date 954094594 -7200
# Node ID 016314c2fa0a5ae8060728150b05e6705055987f
# Parent  34c4847fd8c11fe775e6993aca71373eec5f19cc
tuned;

diff -r 34c4847fd8c1 -r 016314c2fa0a src/HOL/Isar_examples/MultisetOrder.thy
--- 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;
diff -r 34c4847fd8c1 -r 016314c2fa0a src/HOL/Isar_examples/Summation.thy
--- 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 +
diff -r 34c4847fd8c1 -r 016314c2fa0a src/HOL/Isar_examples/document/style.tex
--- 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}}