src/HOL/Bali/Conform.thy
changeset 57983 6edc3529bb4e
parent 57492 74bf65a1910a
child 58887 38db8ddc0f57
     1.1 --- a/src/HOL/Bali/Conform.thy	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/src/HOL/Bali/Conform.thy	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -521,7 +521,7 @@
     1.4  apply auto
     1.5  apply (simp only: obj_ty_cong) 
     1.6  apply (force dest: conforms_globsD intro!: lconf_upd 
     1.7 -       simp add: oconf_def cong del: sum.weak_case_cong)
     1.8 +       simp add: oconf_def cong del: sum.case_cong_weak)
     1.9  done
    1.10  
    1.11  lemma conforms_set_locals: