equal
deleted
inserted
replaced
83 [@{thm de_Morgan_conj}, @{thm de_Morgan_disj}, @{thm imp_disj1}, @{thm imp_disj2}] @ |
83 [@{thm de_Morgan_conj}, @{thm de_Morgan_disj}, @{thm imp_disj1}, @{thm imp_disj2}] @ |
84 @{thms LK_extra_simps}; |
84 @{thms LK_extra_simps}; |
85 |
85 |
86 val LK_ss = |
86 val LK_ss = |
87 LK_basic_ss addsimps LK_simps |
87 LK_basic_ss addsimps LK_simps |
88 addeqcongs [@{thm left_cong}] |
88 |> Simplifier.add_eqcong @{thm left_cong} |
89 addcongs [@{thm imp_cong}]; |
89 |> Simplifier.add_cong @{thm imp_cong}; |
90 |
90 |