src/HOL/Product_Type.thy
changeset 57983 6edc3529bb4e
parent 57233 8fcbfce2a2a9
child 58189 9d714be4f028
     1.1 --- a/src/HOL/Product_Type.thy	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -281,7 +281,7 @@
     1.4  setup {* Sign.parent_path *}
     1.5  
     1.6  declare prod.case [nitpick_simp del]
     1.7 -declare prod.weak_case_cong [cong del]
     1.8 +declare prod.case_cong_weak [cong del]
     1.9  
    1.10  
    1.11  subsubsection {* Tuple syntax *}
    1.12 @@ -486,7 +486,7 @@
    1.13  
    1.14  lemma split_weak_cong: "p = q \<Longrightarrow> split c p = split c q"
    1.15    -- {* Prevents simplification of @{term c}: much faster *}
    1.16 -  by (fact prod.weak_case_cong)
    1.17 +  by (fact prod.case_cong_weak)
    1.18  
    1.19  lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g"
    1.20    by (simp add: split_eta)