ProgTutorial/Tactical.thy
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 *}