| changeset 45620 | f2a587696afb |
| parent 43597 | b4a093e755db |
| child 45625 | 750c5a47400b |
--- a/src/Sequents/simpdata.ML Wed Nov 23 22:07:55 2011 +0100 +++ b/src/Sequents/simpdata.ML Wed Nov 23 22:59:39 2011 +0100 @@ -85,6 +85,6 @@ val LK_ss = LK_basic_ss addsimps LK_simps - addeqcongs [@{thm left_cong}] - addcongs [@{thm imp_cong}]; + |> Simplifier.add_eqcong @{thm left_cong} + |> Simplifier.add_cong @{thm imp_cong};