# HG changeset patch # User blanchet # Date 1276272305 -7200 # Node ID e8c34222814b4d50c164630c55dd7ff5c9675bc4 # Parent cf5e06d5ecaf5f930005e74062494d9fdfab20c4 make test work again (broken since 09467cdfa198?) diff -r cf5e06d5ecaf -r e8c34222814b src/HOL/ex/Meson_Test.thy --- a/src/HOL/ex/Meson_Test.thy Fri Jun 11 17:57:16 2010 +0200 +++ b/src/HOL/ex/Meson_Test.thy Fri Jun 11 18:05:05 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