changeset 240 | d111f5988e49 |
parent 239 | b63c72776f03 |
child 241 | 29d4701c5ee1 |
--- a/ProgTutorial/Tactical.thy Wed Apr 15 13:11:08 2009 +0000 +++ b/ProgTutorial/Tactical.thy Sat Apr 25 14:28:58 2009 +0200 @@ -1475,6 +1475,8 @@ (FIXME: @{ML ObjectLogic.full_atomize_tac}, @{ML ObjectLogic.rulify_tac}) + (FIXME: what are @{ML mksimps_pairs}; used in Nominal.thy) + *} section {* Simprocs *}