changeset 45620 | f2a587696afb |
parent 45594 | d320f2f9f331 |
child 45654 | cf10bde35973 |
--- a/src/FOL/FOL.thy Wed Nov 23 22:07:55 2011 +0100 +++ b/src/FOL/FOL.thy Wed Nov 23 22:59:39 2011 +0100 @@ -339,7 +339,7 @@ FOL_basic_ss addsimps (@{thms meta_simps} @ @{thms IFOL_simps} @ @{thms int_ex_simps} @ @{thms int_all_simps}) addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}] - addcongs [@{thm imp_cong}]; + |> Simplifier.add_cong @{thm imp_cong}; (*classical simprules too*) val FOL_ss = IFOL_ss addsimps (@{thms cla_simps} @ @{thms cla_ex_simps} @ @{thms cla_all_simps});