src/HOL/Bali/Basis.thy
changeset 57983 6edc3529bb4e
parent 55518 1ddb2edf5ceb
child 58249 180f1b3508ed
     1.1 --- a/src/HOL/Bali/Basis.thy	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/src/HOL/Bali/Basis.thy	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5  declare split_if_asm  [split] option.split [split] option.split_asm [split]
     1.6  setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *}
     1.7 -declare if_weak_cong [cong del] option.weak_case_cong [cong del]
     1.8 +declare if_weak_cong [cong del] option.case_cong_weak [cong del]
     1.9  declare length_Suc_conv [iff]
    1.10  
    1.11  lemma Collect_split_eq: "{p. P (split f p)} = {(a,b). P (f a b)}"