# HG changeset patch # User haftmann # Date 1276267937 -7200 # Node ID fe6262d929a3090133e14b5d8b213d3d6b0504f7 # Parent 92a75e6d938b649bad14b44e7cee96fa3df02476 hide sum explicitly diff -r 92a75e6d938b -r fe6262d929a3 src/HOL/ex/Meson_Test.thy --- a/src/HOL/ex/Meson_Test.thy Thu Jun 10 12:28:27 2010 +0200 +++ b/src/HOL/ex/Meson_Test.thy Fri Jun 11 16:52:17 2010 +0200 @@ -16,7 +16,7 @@ below and constants declared in HOL! *} -hide_const (open) subset member quotient union inter +hide_const (open) subset member quotient union inter sum text {* Test data for the MESON proof procedure