| author | Christian Urban <urbanc@in.tum.de> |
| Tue, 06 Oct 2009 16:40:37 +0200 | |
| changeset 333 | 6dea46b9d2da |
| parent 332 | 6fba3a3e80a3 |
| child 334 | 4ae1ecb71539 |
| ProgTutorial/Tactical.thy | file | annotate | diff | comparison | revisions | |
| progtutorial.pdf | file | annotate | diff | comparison | revisions |
--- 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 *}