changeset 8659 | 5fdbe2dd54f9 |
parent 8584 | 016314c2fa0a |
child 8814 | 0a5edcbe0695 |
--- a/src/HOL/Isar_examples/Summation.thy Sat Apr 01 20:22:46 2000 +0200 +++ b/src/HOL/Isar_examples/Summation.thy Sat Apr 01 20:26:20 2000 +0200 @@ -47,8 +47,8 @@ "SUM i < k. b" == "sum (\\<lambda>i. b) k"; -subsection {* Summation laws *}; (*<*) - +subsection {* Summation laws *}; +(*<*) (* FIXME binary arithmetic does not yet work here *) syntax @@ -62,7 +62,6 @@ "6" == "Suc (Suc 4)"; theorems [simp] = add_mult_distrib add_mult_distrib2 mult_ac; - (*>*) text {*