diff -r b63c72776f03 -r d111f5988e49 ProgTutorial/Tactical.thy --- 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 *}