# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1254840037 -7200
# Node ID 6dea46b9d2dae593335261a103e52e8e20511993
# Parent  6fba3a3e80a356477facd8082a791e5e4e68e143
added fixme

diff -r 6fba3a3e80a3 -r 6dea46b9d2da ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Tue Oct 06 11:35:00 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Tue Oct 06 16:40:37 2009 +0200
@@ -1122,6 +1122,8 @@
   run your tactic on the de Bruijn formulae discussed in Exercise~\ref{ex:debruijn}. 
   \end{exercise}
 
+  \footnote{\bf FIXME: explain @{ML_ind Cong_Tac.cong_tac}}
+
 *}
 
 section {* Simplifier Tactics *}
diff -r 6fba3a3e80a3 -r 6dea46b9d2da progtutorial.pdf
Binary file progtutorial.pdf has changed