proper scoping of railaliases;
authorwenzelm
Tue, 06 May 2008 00:10:59 +0200
changeset 26787 4b96f1364138
parent 26786 e4e5d911e01c
child 26788 57b54e586989
proper scoping of railaliases;
doc-src/IsarRef/Thy/pure.thy
doc-src/IsarRef/Thy/syntax.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')
     ;
--- 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}