equal
deleted
inserted
replaced
820 \begin{readmore} |
820 \begin{readmore} |
821 The basic operations on bindings are implemented in |
821 The basic operations on bindings are implemented in |
822 @{ML_file "Pure/General/binding.ML"}. |
822 @{ML_file "Pure/General/binding.ML"}. |
823 \end{readmore} |
823 \end{readmore} |
824 |
824 |
825 \footnote{\bf FIXME give a better example why bindings are important; maybe |
825 \footnote{\bf FIXME give a better example why bindings are important} |
826 give a pointer to \isacommand{local\_setup}; if not, then explain |
826 \footnote{\bf FIXME give a pointer to \isacommand{local\_setup}; if not, then explain |
827 why @{ML snd} is needed.} |
827 why @{ML snd} is needed.} |
828 \footnote{\bf FIXME: There should probably a separate section on binding, long-names |
828 \footnote{\bf FIXME: There should probably a separate section on binding, long-names |
829 and sign.} |
829 and sign.} |
830 |
830 |
831 It is also possible to define your own antiquotations. But you should |
831 It is also possible to define your own antiquotations. But you should |