src/HOL/Old_Number_Theory/Factorization.thy
changeset 57983 6edc3529bb4e
parent 57514 bdc2c6b40bf2
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Old_Number_Theory/Factorization.thy	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/Factorization.thy	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -143,7 +143,7 @@
     1.4    apply (induct xs)
     1.5     apply simp
     1.6     apply (case_tac xs)
     1.7 -    apply (simp_all cong del: list.weak_case_cong)
     1.8 +    apply (simp_all cong del: list.case_cong_weak)
     1.9    done
    1.10  
    1.11  lemma nondec_sort: "nondec (sort xs)"