# HG changeset patch
# User wenzelm
# Date 1304350089 -7200
# Node ID 3a9723fca75cd919cd769e0e33787229675a7bd3
# Parent  9691759a9b3c3ce2ba4868abadd547ae0d35df43
eliminated obsolete rail macros;

diff -r 9691759a9b3c -r 3a9723fca75c doc-src/IsarImplementation/implementation.tex
--- a/doc-src/IsarImplementation/implementation.tex	Mon May 02 17:12:11 2011 +0200
+++ b/doc-src/IsarImplementation/implementation.tex	Mon May 02 17:28:09 2011 +0200
@@ -23,11 +23,6 @@
 
 \makeindex
 
-\railterm{lbrace,rbrace,atsign}
-\railalias{lbracesym}{\isasymlbrace}\railterm{lbracesym}
-\railalias{rbracesym}{\isasymrbrace}\railterm{rbracesym}
-\railalias{dots}{\isasymdots}\railterm{dots}
-
 
 \begin{document}
 
diff -r 9691759a9b3c -r 3a9723fca75c doc-src/IsarRef/isar-ref.tex
--- a/doc-src/IsarRef/isar-ref.tex	Mon May 02 17:12:11 2011 +0200
+++ b/doc-src/IsarRef/isar-ref.tex	Mon May 02 17:28:09 2011 +0200
@@ -36,39 +36,6 @@
 
 \makeindex
 
-\railterm{percent,ppercent,underscore,lbrace,rbrace,atsign}
-\railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
-\railterm{name,nameref,text,type,term,prop,atom}
-
-\railalias{ident}{\railtok{ident}}
-\railalias{longident}{\railtok{longident}}
-\railalias{symident}{\railtok{symident}}
-\railalias{var}{\railtok{var}}
-\railalias{textvar}{\railtok{textvar}}
-\railalias{typefree}{\railtok{typefree}}
-\railalias{typevar}{\railtok{typevar}}
-\railalias{nat}{\railtok{nat}}
-\railalias{string}{\railtok{string}}
-\railalias{verbatim}{\railtok{verbatim}}
-\railalias{keyword}{\railtok{keyword}}
-
-\railalias{name}{\railqtok{name}}
-\railalias{nameref}{\railqtok{nameref}}
-\railalias{text}{\railqtok{text}}
-\railalias{type}{\railqtok{type}}
-\railalias{term}{\railqtok{term}}
-\railalias{prop}{\railqtok{prop}}
-\railalias{atom}{\railqtok{atom}}
-
-\railalias{subseteq}{\isasymsubseteq}\railterm{subseteq}
-\railalias{equiv}{\isasymequiv}\railterm{equiv}
-\railalias{rightleftharpoons}{\isasymrightleftharpoons}\railterm{rightleftharpoons}
-\railalias{rightharpoonup}{\isasymrightharpoonup}\railterm{rightharpoonup}
-\railalias{leftharpoondown}{\isasymleftharpoondown}\railterm{leftharpoondown}
-\railalias{verblbrace}{\texttt{\ttlbrace*}}\railterm{verblbrace}
-\railalias{verbrbrace}{\texttt{*\ttrbrace}}\railterm{verbrbrace}
-
-
 \chardef\charbackquote=`\`
 \newcommand{\backquote}{\mbox{\tt\charbackquote}}
 
diff -r 9691759a9b3c -r 3a9723fca75c doc-src/railsetup.sty
--- a/doc-src/railsetup.sty	Mon May 02 17:12:11 2011 +0200
+++ b/doc-src/railsetup.sty	Mon May 02 17:28:09 2011 +0200
@@ -21,22 +21,9 @@
 {\begin{list}{}{\rail@param}\def\rail@expand{\relax}\makeatletter}{\end{list}}
 
 
-%% old-style content markup
-
-\railalias{percent}{\%}
-\railalias{ppercent}{\%\%}
-\railalias{underscore}{\_}
-\railalias{lbrace}{\texttt{\ttlbrace}}
-\railalias{rbrace}{\texttt{\ttrbrace}}
-\railalias{atsign}{{\at}}
+%% content markup
 
 \def\rail@termfont{\small\ttfamily\upshape\isabellestyle{tt}}
-\def\rail@tokenfont{\small\ttfamily\upshape}
 \def\rail@nontfont{\small\rmfamily\upshape\isabellestyle{it}}
-\def\rail@annofont{\small\rmfamily\itshape}
 \def\rail@namefont{\small\rmfamily\itshape\isabellestyle{it}}
-\def\rail@indexfont{\small\rmfamily\itshape}
-\newcommand{\railtterm}[1]{{\texttt{#1}}}
-\newcommand{\railtok}[1]{{\textrm{#1}}}
-\newcommand{\railqtok}[1]{{\rmfamily\textsl{#1}}}
-\newcommand{\railnonterm}[1]{{\emph{#1}}}
+