src/HOL/Product_Type.thy
changeset 37411 c88c44156083
parent 37389 09467cdfa198
child 37591 d3daea901123
     1.1 --- a/src/HOL/Product_Type.thy	Fri Jun 11 16:52:17 2010 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Mon Jun 14 15:10:36 2010 +0200
     1.3 @@ -158,6 +158,8 @@
     1.4      by (simp add: Pair_def Abs_prod_inject)
     1.5  qed
     1.6  
     1.7 +declare weak_case_cong [cong del]
     1.8 +
     1.9  
    1.10  subsubsection {* Tuple syntax *}
    1.11