# HG changeset patch
# User nipkow
# Date 1089898791 -7200
# Node ID 82fb871517186efa953b7ae0ca112b9f343c2926
# Parent  11b4dce71d7377e8be0c192786e32c80936f7c2f
more summation syntax

diff -r 11b4dce71d73 -r 82fb87151718 src/HOL/Isar_examples/HoareEx.thy
--- a/src/HOL/Isar_examples/HoareEx.thy	Thu Jul 15 15:39:40 2004 +0200
+++ b/src/HOL/Isar_examples/HoareEx.thy	Thu Jul 15 15:39:51 2004 +0200
@@ -180,18 +180,6 @@
  the problem.
 *}
 
-consts
-  sum :: "(nat => nat) => nat => nat"
-primrec
-  "sum f 0 = 0"
-  "sum f (Suc n) = f n + sum f n"
-
-syntax
-  "_sum" :: "idt => nat => nat => nat"
-    ("SUM _<_. _" [0, 0, 10] 10)
-translations
-  "SUM j<k. b" == "sum (\<lambda>j. b) k"
-
 text {*
  The following proof is quite explicit in the individual steps taken,
  with the \name{hoare} method only applied locally to take care of
@@ -211,8 +199,8 @@
       .{\<acute>S = (SUM j<n. j)}."
   (is "|- _ (_; ?while) _")
 proof -
-  let ?sum = "\<lambda>k. SUM j<k. j"
-  let ?inv = "\<lambda>s i. s = ?sum i"
+  let ?sum = "\<lambda>k::nat. SUM j<k. j"
+  let ?inv = "\<lambda>s i::nat. s = ?sum i"
 
   have "|- .{True}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}."
   proof -
@@ -252,8 +240,8 @@
       OD
       .{\<acute>S = (SUM j<n. j)}."
 proof -
-  let ?sum = "\<lambda>k. SUM j<k. j"
-  let ?inv = "\<lambda>s i. s = ?sum i"
+  let ?sum = "\<lambda>k::nat. SUM j<k. j"
+  let ?inv = "\<lambda>s i::nat. s = ?sum i"
 
   show ?thesis
   proof hoare