1.1 --- a/doc-src/antiquote_setup.ML Wed Jun 10 11:29:57 2009 +0200
1.2 +++ b/doc-src/antiquote_setup.ML Wed Jun 10 11:31:26 2009 +0200
1.3 @@ -19,16 +19,16 @@
1.4 | "{" => "\\{"
1.5 | "|" => "$\\mid$"
1.6 | "}" => "\\}"
1.7 - | "\\<dash>" => "-"
1.8 + | "\<dash>" => "-"
1.9 | c => c);
1.10
1.11 -fun clean_name "\\<dots>" = "dots"
1.12 +fun clean_name "\<dots>" = "dots"
1.13 | clean_name ".." = "ddot"
1.14 | clean_name "." = "dot"
1.15 | clean_name "_" = "underscore"
1.16 | clean_name "{" = "braceleft"
1.17 | clean_name "}" = "braceright"
1.18 - | clean_name s = s |> translate (fn "_" => "-" | "\\<dash>" => "-" | c => c);
1.19 + | clean_name s = s |> translate (fn "_" => "-" | "\<dash>" => "-" | c => c);
1.20
1.21
1.22 (* verbatim text *)