1.1 --- a/src/HOL/Product_Type.thy Mon Oct 17 18:05:14 2011 +0200
1.2 +++ b/src/HOL/Product_Type.thy Tue Oct 18 15:19:06 2011 +0200
1.3 @@ -1228,4 +1228,6 @@
1.4
1.5 lemmas Pair_fst_snd_eq = prod_eq_iff
1.6
1.7 +hide_const (open) prod
1.8 +
1.9 end
2.1 --- a/src/HOL/Sum_Type.thy Mon Oct 17 18:05:14 2011 +0200
2.2 +++ b/src/HOL/Sum_Type.thy Tue Oct 18 15:19:06 2011 +0200
2.3 @@ -209,4 +209,6 @@
2.4
2.5 hide_const (open) Suml Sumr Projl Projr
2.6
2.7 +hide_const (open) sum
2.8 +
2.9 end
3.1 --- a/src/HOL/ex/Meson_Test.thy Mon Oct 17 18:05:14 2011 +0200
3.2 +++ b/src/HOL/ex/Meson_Test.thy Tue Oct 18 15:19:06 2011 +0200
3.3 @@ -10,7 +10,7 @@
3.4 below and constants declared in HOL!
3.5 *}
3.6
3.7 -hide_const (open) implies union inter subset sum quotient
3.8 +hide_const (open) implies union inter subset quotient
3.9
3.10 text {*
3.11 Test data for the MESON proof procedure