--- a/src/HOL/Product_Type.thy Mon Oct 17 18:05:14 2011 +0200
+++ b/src/HOL/Product_Type.thy Tue Oct 18 15:19:06 2011 +0200
@@ -1228,4 +1228,6 @@
lemmas Pair_fst_snd_eq = prod_eq_iff
+hide_const (open) prod
+
end
--- a/src/HOL/Sum_Type.thy Mon Oct 17 18:05:14 2011 +0200
+++ b/src/HOL/Sum_Type.thy Tue Oct 18 15:19:06 2011 +0200
@@ -209,4 +209,6 @@
hide_const (open) Suml Sumr Projl Projr
+hide_const (open) sum
+
end
--- a/src/HOL/ex/Meson_Test.thy Mon Oct 17 18:05:14 2011 +0200
+++ b/src/HOL/ex/Meson_Test.thy Tue Oct 18 15:19:06 2011 +0200
@@ -10,7 +10,7 @@
below and constants declared in HOL!
*}
-hide_const (open) implies union inter subset sum quotient
+hide_const (open) implies union inter subset quotient
text {*
Test data for the MESON proof procedure