doc-src/IsarRef/isar-ref.tex
changeset 42620 3a9723fca75c
parent 42511 bf89455ccf9d
child 42632 ebec0c1a5984
--- 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}}