src/HOL/Product_Type.thy
changeset 40929 7ff03a5e044f
parent 40702 cf26dd7395e4
child 40968 a6fcd305f7dc
     1.1 --- a/src/HOL/Product_Type.thy	Fri Dec 03 10:03:10 2010 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Fri Dec 03 10:03:13 2010 +0100
     1.3 @@ -160,7 +160,7 @@
     1.4  
     1.5  declare prod.simps(2) [nitpick_simp del]
     1.6  
     1.7 -declare weak_case_cong [cong del]
     1.8 +declare prod.weak_case_cong [cong del]
     1.9  
    1.10  
    1.11  subsubsection {* Tuple syntax *}
    1.12 @@ -440,7 +440,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 weak_case_cong)
    1.17 +  by (fact prod.weak_case_cong)
    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)
    1.21 @@ -578,7 +578,7 @@
    1.22    \medskip @{term split} used as a logical connective or set former.
    1.23  
    1.24    \medskip These rules are for use with @{text blast}; could instead
    1.25 -  call @{text simp} using @{thm [source] split} as rewrite. *}
    1.26 +  call @{text simp} using @{thm [source] prod.split} as rewrite. *}
    1.27  
    1.28  lemma splitI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> split c p"
    1.29    apply (simp only: split_tupled_all)