# HG changeset patch
# User nipkow
# Date 1483986760 -3600
# Node ID 33aab75ff4238049bd61a90513ce266b2ccf2114
# Parent  54f5afc9c41389d3339a5491790249c33ee165ac
hide global sum

diff -r 54f5afc9c413 -r 33aab75ff423 src/HOL/IMP/Hoare_Examples.thy
--- a/src/HOL/IMP/Hoare_Examples.thy	Mon Jan 09 15:54:48 2017 +0000
+++ b/src/HOL/IMP/Hoare_Examples.thy	Mon Jan 09 19:32:40 2017 +0100
@@ -2,6 +2,8 @@
 
 theory Hoare_Examples imports Hoare begin
 
+hide_const (open) sum
+
 text{* Summing up the first @{text x} natural numbers in variable @{text y}. *}
 
 fun sum :: "int \<Rightarrow> int" where