equal
deleted
inserted
replaced
124 \%%% TeX-master: \"root\"\n\ |
124 \%%% TeX-master: \"root\"\n\ |
125 \%%% End:\n"; |
125 \%%% End:\n"; |
126 |
126 |
127 fun isabelle_file name txt = |
127 fun isabelle_file name txt = |
128 "%\n\\begin{isabellebody}%\n\ |
128 "%\n\\begin{isabellebody}%\n\ |
129 \\\def\\isabellecontext{" ^ name ^ "}%\n" ^ txt ^ |
129 \\\def\\isabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^ |
130 "\\end{isabellebody}%\n" ^ tex_trailer; |
130 "\\end{isabellebody}%\n" ^ tex_trailer; |
131 |
131 |
132 fun old_symbol_source name syms = |
132 fun old_symbol_source name syms = |
133 isabelle_file name ("\\isamarkupheader{" ^ output_syms name ^ "}%\n" ^ output_symbols syms); |
133 isabelle_file name ("\\isamarkupheader{" ^ output_syms name ^ "}%\n" ^ output_symbols syms); |
134 |
134 |