# HG changeset patch
# User wenzelm
# Date 1210025459 -7200
# Node ID 4b96f1364138edebab4220080bcf883b0c089c22
# Parent  e4e5d911e01cc10210b17d18c78f9e89e401ae73
proper scoping of railaliases;

diff -r e4e5d911e01c -r 4b96f1364138 doc-src/IsarRef/Thy/pure.thy
--- a/doc-src/IsarRef/Thy/pure.thy	Tue May 06 00:10:23 2008 +0200
+++ b/doc-src/IsarRef/Thy/pure.thy	Tue May 06 00:10:59 2008 +0200
@@ -368,15 +368,6 @@
     @{command_def "no_translations"} & : & \isartrans{theory}{theory} \\
   \end{matharray}
 
-  \railalias{rightleftharpoons}{\isasymrightleftharpoons}
-  \railterm{rightleftharpoons}
-
-  \railalias{rightharpoonup}{\isasymrightharpoonup}
-  \railterm{rightharpoonup}
-
-  \railalias{leftharpoondown}{\isasymleftharpoondown}
-  \railterm{leftharpoondown}
-
   \begin{rail}
     ('syntax' | 'no\_syntax') mode? (constdecl +)
     ;
@@ -777,9 +768,6 @@
   exporting some result @{text "x \<equiv> t \<turnstile> \<phi>[x]"} yields @{text "\<turnstile>
   \<phi>[t]"}.
 
-  \railalias{equiv}{\isasymequiv}
-  \railterm{equiv}
-
   \begin{rail}
     'fix' (vars + 'and')
     ;
diff -r e4e5d911e01c -r 4b96f1364138 doc-src/IsarRef/Thy/syntax.thy
--- a/doc-src/IsarRef/Thy/syntax.thy	Tue May 06 00:10:23 2008 +0200
+++ b/doc-src/IsarRef/Thy/syntax.thy	Tue May 06 00:10:59 2008 +0200
@@ -197,9 +197,6 @@
   intersection of these classes.  The syntax of type arities is given
   directly at the outer level.
 
-  \railalias{subseteq}{\isasymsubseteq}
-  \railterm{subseteq}
-
   \indexouternonterm{sort}\indexouternonterm{arity}
   \indexouternonterm{classdecl}
   \begin{rail}