hide typedef-generated constants Product_Type.prod and Sum_Type.sum
authorhuffman
Tue Oct 18 15:19:06 2011 +0200 (2011-10-18)
changeset 452045e4a1270c000
parent 45161 699848baf70b
child 45205 2825ce94fd4d
hide typedef-generated constants Product_Type.prod and Sum_Type.sum
src/HOL/Product_Type.thy
src/HOL/Sum_Type.thy
src/HOL/ex/Meson_Test.thy
     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