# 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 \ t \ \[x]"} yields @{text "\ \[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}