changeset 45620 | f2a587696afb |
parent 45614 | e19788cb0a1a |
child 45625 | 750c5a47400b |
--- a/NEWS Wed Nov 23 22:07:55 2011 +0100 +++ b/NEWS Wed Nov 23 22:59:39 2011 +0100 @@ -167,6 +167,15 @@ change of semantics: update is applied to auxiliary local theory context as well. +* Modernized some old-style infix operations: + + addeqcongs ~> Simplifier.add_eqcong + deleqcongs ~> Simplifier.del_eqcong + addcongs ~> Simplifier.add_cong + delcongs ~> Simplifier.del_cong + addsplits ~> Splitter.add_split + delsplits ~> Splitter.del_split + New in Isabelle2011-1 (October 2011)