author wenzelm Sun, 26 Mar 2000 20:16:34 +0200 changeset 8584 016314c2fa0a parent 8583 34c4847fd8c1 child 8585 8a3ae21e4a5b
tuned;
--- 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 @@

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\$