changeset 361 | 8ba963a3e039 |
parent 359 | be6538c7b41d |
child 362 | a5e7ab090abf |
--- a/ProgTutorial/Tactical.thy Mon Oct 26 00:00:26 2009 +0100 +++ b/ProgTutorial/Tactical.thy Tue Oct 27 15:43:21 2009 +0100 @@ -1592,9 +1592,6 @@ (FIXME: Anything interesting to say about @{ML Simplifier.clear_ss}?) - (FIXME: @{ML ObjectLogic.full_atomize_tac}, - @{ML ObjectLogic.rulify_tac}) - (FIXME: what are @{ML mksimps_pairs}; used in Nominal.thy) (FIXME: explain @{ML simplify} and @{ML "Simplifier.rewrite_rule"} etc.)