Mercurialisabelle / diff
summary | shortlog | changelog | graph | tags | branches | files | changeset | file | revisions | annotate | diff | raw
src/Pure/Thy/latex.ML
changeset 14361 ad2f5da643b4
parent 11860 36ba0d4a836c
child 14364 fc62df0bf353 
     1.1 --- a/src/Pure/Thy/latex.ML	Sun Jan 25 00:42:22 2004 +0100
     1.2 +++ b/src/Pure/Thy/latex.ML	Mon Jan 26 10:34:02 2004 +0100
     1.3 @@ -69,7 +69,8 @@
     1.4    if size s = 1 then output_chr s
     1.5    else
     1.6      (case explode s of
     1.7 -      "\\" :: "<" :: "^" :: cs => "\\isactrl" ^ implode (#1 (Library.split_last cs)) ^ " "
     1.8 +      "\\" :: "<" :: "^" :: "r"::"a"::"w":: cs => implode (#1 (Library.split_last cs)) ^ " "
     1.9 +    | "\\" :: "<" :: "^" :: cs => "\\isactrl" ^ implode (#1 (Library.split_last cs)) ^ " "
    1.10      | "\\" :: "<" :: cs => "{\\isasym" ^ implode (#1 (Library.split_last cs)) ^ "}"
    1.11      | _ => sys_error "output_sym");
    1.12
isabelle