doc-src/IsarRef/Thy/syntax.thy
changeset 26787 4b96f1364138
parent 26777 134529bc72db
child 26957 e3f04fdd994d
equal deleted inserted replaced
26786:e4e5d911e01c 26787:4b96f1364138
   194   Classes are specified by plain names.  Sorts have a very simple
   194   Classes are specified by plain names.  Sorts have a very simple
   195   inner syntax, which is either a single class name @{text c} or a
   195   inner syntax, which is either a single class name @{text c} or a
   196   list @{text "{c\<^sub>1, \<dots>, c\<^sub>n}"} referring to the
   196   list @{text "{c\<^sub>1, \<dots>, c\<^sub>n}"} referring to the
   197   intersection of these classes.  The syntax of type arities is given
   197   intersection of these classes.  The syntax of type arities is given
   198   directly at the outer level.
   198   directly at the outer level.
   199 
       
   200   \railalias{subseteq}{\isasymsubseteq}
       
   201   \railterm{subseteq}
       
   202 
   199 
   203   \indexouternonterm{sort}\indexouternonterm{arity}
   200   \indexouternonterm{sort}\indexouternonterm{arity}
   204   \indexouternonterm{classdecl}
   201   \indexouternonterm{classdecl}
   205   \begin{rail}
   202   \begin{rail}
   206     classdecl: name (('<' | subseteq) (nameref + ','))?
   203     classdecl: name (('<' | subseteq) (nameref + ','))?