equal
deleted
inserted
replaced
808 \indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\ |
808 \indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\ |
809 \indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
809 \indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
810 \end{matharray} |
810 \end{matharray} |
811 |
811 |
812 \begin{mldecls} |
812 \begin{mldecls} |
813 \indexml{bind\_thms}\verb|bind_thms: string * thm list -> unit| \\ |
813 \indexdef{}{ML}{bind\_thms}\verb|bind_thms: string * thm list -> unit| \\ |
814 \indexml{bind\_thm}\verb|bind_thm: string * thm -> unit| \\ |
814 \indexdef{}{ML}{bind\_thm}\verb|bind_thm: string * thm -> unit| \\ |
815 \end{mldecls} |
815 \end{mldecls} |
816 |
816 |
817 \begin{rail} |
817 \begin{rail} |
818 'use' name |
818 'use' name |
819 ; |
819 ; |