lib/Tools/mkdir
changeset 28180 3f69c3c54478
parent 25410 0ba2d51bcb42
child 28500 4b79e5d3d0aa
equal deleted inserted replaced
28179:8e8313aededc 28180:3f69c3c54478
   240 
   240 
   241 % urls in roman style, theory text in math-similar italics
   241 % urls in roman style, theory text in math-similar italics
   242 \urlstyle{rm}
   242 \urlstyle{rm}
   243 \isabellestyle{it}
   243 \isabellestyle{it}
   244 
   244 
       
   245 % for uniform font size
       
   246 %\renewcommand{\isastyle}{\isastyleminor}
       
   247 
   245 
   248 
   246 \begin{document}
   249 \begin{document}
   247 
   250 
   248 \title{$TITLE}
   251 \title{$TITLE}
   249 \author{$AUTHOR}
   252 \author{$AUTHOR}