Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/Ref/ref.rao
author wenzelm
Fri, 19 Dec 1997 09:58:42 +0100
changeset 4439 02730662e446
parent 4316 86ac9153e660
child 4543 82a45bdd0e80
permissions -rw-r--r--
Term.termless;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
     1
 
% This file was generated by 'rail' from 'ref.rai'
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
     2
 
\rail@t {lbrace}
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
     3
 
\rail@t {rbrace}
4316
wenzelm
parents: 3213
diff changeset 
     4
 
\rail@i {1}{ \par theoryDef : id '=' (name + '+') ('+' extension | ()) ; \par name: id | string ; \par extension : (section +) 'end' ( () | ml ) ; \par section : classes | default | types | arities | consts | syntax | trans | defs | constdefs | rules | axclass | instance | oracle ; \par classes : 'classes' ( classDecl + ) ; \par classDecl : (id (() | '<' (id + ','))) ; \par default : 'default' sort ; \par sort : id | lbrace (id * ',') rbrace ; \par types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + ) ; \par infix : ( 'infixr' | 'infixl' ) (() | string) nat ; \par typeDecl : typevarlist name ( () | '=' ( string | type ) ); \par typevarlist : () | tid | '(' ( tid + ',' ) ')'; \par type : simpleType | '(' type ')' | type '=>' type | '[' ( type + "," ) ']' '=>' type; \par simpleType: id | ( tid ( () | '::' id ) ) | '(' ( type + "," ) ')' id | simpleType id ; \par arities : 'arities' ((name + ',') '::' arity +) ; \par arity : ( () | '(' (sort + ',') ')' ) sort ; \par consts : 'consts' ( mixfixConstDecl + ) ; \par syntax : 'syntax' (() | mode) ( mixfixConstDecl + ); \par mode : '(' name (() | 'output') ')' ; \par mixfixConstDecl : constDecl (() | ( '(' mixfix ')' )) ; \par constDecl : ( name + ',') '::' (string | type); \par mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat ) | infix | 'binder' string nat ; \par trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + ) ; \par pat : ( () | ( '(' id ')' ) ) string; \par rules : 'rules' (( id string ) + ) ; \par defs : 'defs' (( id string ) + ) ; \par constdefs : 'constdefs' (id '::' (string | type) string +) ; \par axclass : 'axclass' classDecl (() | ( id string ) +) ; \par instance : 'instance' ( name '<' name | name '::' arity) witness ; \par witness : (() | '(' ((string | longident) + ',') ')') (() | verbatim) ; \par oracle : 'oracle' name '=' name ; \par ml : 'ML' text ; \par }
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
     5
 
\rail@o {1}{
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
     6
 
\rail@begin{2}{theoryDef}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
     7
 
\rail@nont{id}[]
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
     8
 
\rail@term{=}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
     9
 
\rail@plus
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    10
 
\rail@nont{name}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    11
 
\rail@nextplus{1}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    12
 
\rail@cterm{+}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    13
 
\rail@endplus
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    14
 
\rail@bar
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    15
 
\rail@term{+}[]
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    16
 
\rail@nont{extension}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    17
 
\rail@nextbar{1}
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    18
 
\rail@endbar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    19
 
\rail@end
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    20
 
\rail@begin{2}{name}
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    21
 
\rail@bar
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    22
 
\rail@nont{id}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    23
 
\rail@nextbar{1}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    24
 
\rail@nont{string}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    25
 
\rail@endbar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    26
 
\rail@end
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    27
 
\rail@begin{2}{extension}
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    28
 
\rail@plus
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    29
 
\rail@nont{section}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    30
 
\rail@nextplus{1}
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    31
 
\rail@endplus
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    32
 
\rail@term{end}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    33
 
\rail@bar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    34
 
\rail@nextbar{1}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    35
 
\rail@nont{ml}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    36
 
\rail@endbar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    37
 
\rail@end
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
    38
 
\rail@begin{13}{section}
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    39
 
\rail@bar
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    40
 
\rail@nont{classes}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    41
 
\rail@nextbar{1}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    42
 
\rail@nont{default}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    43
 
\rail@nextbar{2}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    44
 
\rail@nont{types}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    45
 
\rail@nextbar{3}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    46
 
\rail@nont{arities}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    47
 
\rail@nextbar{4}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    48
 
\rail@nont{consts}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    49
 
\rail@nextbar{5}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
    50
 
\rail@nont{syntax}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    51
 
\rail@nextbar{6}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    52
 
\rail@nont{trans}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    53
 
\rail@nextbar{7}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    54
 
\rail@nont{defs}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    55
 
\rail@nextbar{8}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
    56
 
\rail@nont{constdefs}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
    57
 
\rail@nextbar{9}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    58
 
\rail@nont{rules}[]
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
    59
 
\rail@nextbar{10}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
    60
 
\rail@nont{axclass}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
    61
 
\rail@nextbar{11}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
    62
 
\rail@nont{instance}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
    63
 
\rail@nextbar{12}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    64
 
\rail@nont{oracle}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    65
 
\rail@endbar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    66
 
\rail@end
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
    67
 
\rail@begin{2}{classes}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    68
 
\rail@term{classes}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    69
 
\rail@plus
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
    70
 
\rail@nont{classDecl}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
    71
 
\rail@nextplus{1}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
    72
 
\rail@endplus
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
    73
 
\rail@end
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
    74
 
\rail@begin{3}{classDecl}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    75
 
\rail@nont{id}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    76
 
\rail@bar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    77
 
\rail@nextbar{1}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    78
 
\rail@term{<}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    79
 
\rail@plus
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    80
 
\rail@nont{id}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    81
 
\rail@nextplus{2}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    82
 
\rail@cterm{,}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    83
 
\rail@endplus
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    84
 
\rail@endbar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    85
 
\rail@end
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    86
 
\rail@begin{1}{default}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    87
 
\rail@term{default}[]
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    88
 
\rail@nont{sort}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    89
 
\rail@end
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    90
 
\rail@begin{4}{sort}
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    91
 
\rail@bar
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    92
 
\rail@nont{id}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    93
 
\rail@nextbar{1}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    94
 
\rail@token{lbrace}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    95
 
\rail@bar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    96
 
\rail@nextbar{2}
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    97
 
\rail@plus
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
    98
 
\rail@nont{id}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
    99
 
\rail@nextplus{3}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   100
 
\rail@cterm{,}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   101
 
\rail@endplus
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   102
 
\rail@endbar
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   103
 
\rail@token{rbrace}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   104
 
\rail@endbar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   105
 
\rail@end
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   106
 
\rail@begin{3}{types}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   107
 
\rail@term{types}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   108
 
\rail@plus
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   109
 
\rail@nont{typeDecl}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   110
 
\rail@bar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   111
 
\rail@nextbar{1}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   112
 
\rail@term{(}[]
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   113
 
\rail@nont{infix}[]
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   114
 
\rail@term{)}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   115
 
\rail@endbar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   116
 
\rail@nextplus{2}
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   117
 
\rail@endplus
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   118
 
\rail@end
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   119
 
\rail@begin{2}{infix}
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   120
 
\rail@bar
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   121
 
\rail@term{infixr}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   122
 
\rail@nextbar{1}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   123
 
\rail@term{infixl}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   124
 
\rail@endbar
3213
wenzelm
parents: 3129
diff changeset 
   125
 
\rail@bar
wenzelm
parents: 3129
diff changeset 
   126
 
\rail@nextbar{1}
wenzelm
parents: 3129
diff changeset 
   127
 
\rail@nont{string}[]
wenzelm
parents: 3129
diff changeset 
   128
 
\rail@endbar
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   129
 
\rail@nont{nat}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   130
 
\rail@end
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   131
 
\rail@begin{3}{typeDecl}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   132
 
\rail@nont{typevarlist}[]
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   133
 
\rail@nont{name}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   134
 
\rail@bar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   135
 
\rail@nextbar{1}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   136
 
\rail@term{=}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   137
 
\rail@bar
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   138
 
\rail@nont{string}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   139
 
\rail@nextbar{2}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   140
 
\rail@nont{type}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   141
 
\rail@endbar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   142
 
\rail@endbar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   143
 
\rail@end
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   144
 
\rail@begin{4}{typevarlist}
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   145
 
\rail@bar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   146
 
\rail@nextbar{1}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   147
 
\rail@nont{tid}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   148
 
\rail@nextbar{2}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   149
 
\rail@term{(}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   150
 
\rail@plus
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   151
 
\rail@nont{tid}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   152
 
\rail@nextplus{3}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   153
 
\rail@cterm{,}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   154
 
\rail@endplus
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   155
 
\rail@term{)}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   156
 
\rail@endbar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   157
 
\rail@end
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   158
 
\rail@begin{5}{type}
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   159
 
\rail@bar
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   160
 
\rail@nont{simpleType}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   161
 
\rail@nextbar{1}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   162
 
\rail@term{(}[]
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   163
 
\rail@nont{type}[]
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   164
 
\rail@term{)}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   165
 
\rail@nextbar{2}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   166
 
\rail@nont{type}[]
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   167
 
\rail@term{=>}[]
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   168
 
\rail@nont{type}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   169
 
\rail@nextbar{3}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   170
 
\rail@term{[}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   171
 
\rail@plus
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   172
 
\rail@nont{type}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   173
 
\rail@nextplus{4}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   174
 
\rail@cterm{,}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   175
 
\rail@endplus
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   176
 
\rail@term{]}[]
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   177
 
\rail@term{=>}[]
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   178
 
\rail@nont{type}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   179
 
\rail@endbar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   180
 
\rail@end
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   181
 
\rail@begin{6}{simpleType}
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   182
 
\rail@bar
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   183
 
\rail@nont{id}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   184
 
\rail@nextbar{1}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   185
 
\rail@nont{tid}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   186
 
\rail@bar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   187
 
\rail@nextbar{2}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   188
 
\rail@term{::}[]
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   189
 
\rail@nont{id}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   190
 
\rail@endbar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   191
 
\rail@nextbar{3}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   192
 
\rail@term{(}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   193
 
\rail@plus
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   194
 
\rail@nont{type}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   195
 
\rail@nextplus{4}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   196
 
\rail@cterm{,}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   197
 
\rail@endplus
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   198
 
\rail@term{)}[]
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   199
 
\rail@nont{id}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   200
 
\rail@nextbar{5}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   201
 
\rail@nont{simpleType}[]
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   202
 
\rail@nont{id}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   203
 
\rail@endbar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   204
 
\rail@end
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   205
 
\rail@begin{3}{arities}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   206
 
\rail@term{arities}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   207
 
\rail@plus
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   208
 
\rail@plus
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   209
 
\rail@nont{name}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   210
 
\rail@nextplus{1}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   211
 
\rail@cterm{,}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   212
 
\rail@endplus
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   213
 
\rail@term{::}[]
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   214
 
\rail@nont{arity}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   215
 
\rail@nextplus{2}
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   216
 
\rail@endplus
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   217
 
\rail@end
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   218
 
\rail@begin{3}{arity}
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   219
 
\rail@bar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   220
 
\rail@nextbar{1}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   221
 
\rail@term{(}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   222
 
\rail@plus
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   223
 
\rail@nont{sort}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   224
 
\rail@nextplus{2}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   225
 
\rail@cterm{,}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   226
 
\rail@endplus
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   227
 
\rail@term{)}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   228
 
\rail@endbar
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   229
 
\rail@nont{sort}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   230
 
\rail@end
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   231
 
\rail@begin{2}{consts}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   232
 
\rail@term{consts}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   233
 
\rail@plus
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   234
 
\rail@nont{mixfixConstDecl}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   235
 
\rail@nextplus{1}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   236
 
\rail@endplus
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   237
 
\rail@end
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   238
 
\rail@begin{2}{syntax}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   239
 
\rail@term{syntax}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   240
 
\rail@bar
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   241
 
\rail@nextbar{1}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   242
 
\rail@nont{mode}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   243
 
\rail@endbar
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   244
 
\rail@plus
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   245
 
\rail@nont{mixfixConstDecl}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   246
 
\rail@nextplus{1}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   247
 
\rail@endplus
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   248
 
\rail@end
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   249
 
\rail@begin{2}{mode}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   250
 
\rail@term{(}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   251
 
\rail@nont{name}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   252
 
\rail@bar
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   253
 
\rail@nextbar{1}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   254
 
\rail@term{output}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   255
 
\rail@endbar
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   256
 
\rail@term{)}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   257
 
\rail@end
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   258
 
\rail@begin{2}{mixfixConstDecl}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   259
 
\rail@nont{constDecl}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   260
 
\rail@bar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   261
 
\rail@nextbar{1}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   262
 
\rail@term{(}[]
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   263
 
\rail@nont{mixfix}[]
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   264
 
\rail@term{)}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   265
 
\rail@endbar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   266
 
\rail@end
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   267
 
\rail@begin{2}{constDecl}
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   268
 
\rail@plus
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   269
 
\rail@nont{name}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   270
 
\rail@nextplus{1}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   271
 
\rail@cterm{,}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   272
 
\rail@endplus
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   273
 
\rail@term{::}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   274
 
\rail@bar
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   275
 
\rail@nont{string}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   276
 
\rail@nextbar{1}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   277
 
\rail@nont{type}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   278
 
\rail@endbar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   279
 
\rail@end
3213
wenzelm
parents: 3129
diff changeset 
   280
 
\rail@begin{6}{mixfix}
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   281
 
\rail@bar
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   282
 
\rail@nont{string}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   283
 
\rail@bar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   284
 
\rail@nextbar{1}
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   285
 
\rail@bar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   286
 
\rail@nextbar{2}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   287
 
\rail@term{[}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   288
 
\rail@plus
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   289
 
\rail@nont{nat}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   290
 
\rail@nextplus{3}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   291
 
\rail@cterm{,}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   292
 
\rail@endplus
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   293
 
\rail@term{]}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   294
 
\rail@endbar
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   295
 
\rail@nont{nat}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   296
 
\rail@endbar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   297
 
\rail@nextbar{4}
3213
wenzelm
parents: 3129
diff changeset 
   298
 
\rail@nont{infix}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   299
 
\rail@nextbar{5}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   300
 
\rail@term{binder}[]
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   301
 
\rail@nont{string}[]
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   302
 
\rail@nont{nat}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   303
 
\rail@endbar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   304
 
\rail@end
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   305
 
\rail@begin{4}{trans}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   306
 
\rail@term{translations}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   307
 
\rail@plus
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   308
 
\rail@nont{pat}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   309
 
\rail@bar
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   310
 
\rail@term{==}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   311
 
\rail@nextbar{1}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   312
 
\rail@term{=>}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   313
 
\rail@nextbar{2}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   314
 
\rail@term{<=}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   315
 
\rail@endbar
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   316
 
\rail@nont{pat}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   317
 
\rail@nextplus{3}
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   318
 
\rail@endplus
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   319
 
\rail@end
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   320
 
\rail@begin{2}{pat}
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   321
 
\rail@bar
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   322
 
\rail@nextbar{1}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   323
 
\rail@term{(}[]
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   324
 
\rail@nont{id}[]
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   325
 
\rail@term{)}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   326
 
\rail@endbar
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   327
 
\rail@nont{string}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   328
 
\rail@end
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   329
 
\rail@begin{2}{rules}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   330
 
\rail@term{rules}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   331
 
\rail@plus
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   332
 
\rail@nont{id}[]
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   333
 
\rail@nont{string}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   334
 
\rail@nextplus{1}
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   335
 
\rail@endplus
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   336
 
\rail@end
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   337
 
\rail@begin{2}{defs}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   338
 
\rail@term{defs}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   339
 
\rail@plus
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   340
 
\rail@nont{id}[]
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   341
 
\rail@nont{string}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   342
 
\rail@nextplus{1}
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   343
 
\rail@endplus
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   344
 
\rail@end
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   345
 
\rail@begin{3}{constdefs}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   346
 
\rail@term{constdefs}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   347
 
\rail@plus
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   348
 
\rail@nont{id}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   349
 
\rail@term{::}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   350
 
\rail@bar
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   351
 
\rail@nont{string}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   352
 
\rail@nextbar{1}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   353
 
\rail@nont{type}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   354
 
\rail@endbar
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   355
 
\rail@nont{string}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   356
 
\rail@nextplus{2}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   357
 
\rail@endplus
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   358
 
\rail@end
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   359
 
\rail@begin{3}{axclass}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   360
 
\rail@term{axclass}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   361
 
\rail@nont{classDecl}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   362
 
\rail@bar
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   363
 
\rail@nextbar{1}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   364
 
\rail@plus
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   365
 
\rail@nont{id}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   366
 
\rail@nont{string}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   367
 
\rail@nextplus{2}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   368
 
\rail@endplus
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   369
 
\rail@endbar
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   370
 
\rail@end
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   371
 
\rail@begin{2}{instance}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   372
 
\rail@term{instance}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   373
 
\rail@bar
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   374
 
\rail@nont{name}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   375
 
\rail@term{<}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   376
 
\rail@nont{name}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   377
 
\rail@nextbar{1}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   378
 
\rail@nont{name}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   379
 
\rail@term{::}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   380
 
\rail@nont{arity}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   381
 
\rail@endbar
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   382
 
\rail@nont{witness}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   383
 
\rail@end
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   384
 
\rail@begin{4}{witness}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   385
 
\rail@bar
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   386
 
\rail@nextbar{1}
3129
wenzelm
parents: 3108
diff changeset 
   387
 
\rail@term{(}[]
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   388
 
\rail@plus
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   389
 
\rail@bar
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   390
 
\rail@nont{string}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   391
 
\rail@nextbar{2}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   392
 
\rail@nont{longident}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   393
 
\rail@endbar
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   394
 
\rail@nextplus{3}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   395
 
\rail@cterm{,}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   396
 
\rail@endplus
3129
wenzelm
parents: 3108
diff changeset 
   397
 
\rail@term{)}[]
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   398
 
\rail@endbar
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   399
 
\rail@bar
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   400
 
\rail@nextbar{1}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   401
 
\rail@nont{verbatim}[]
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   402
 
\rail@endbar
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset 
   403
 
\rail@end
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   404
 
\rail@begin{1}{oracle}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   405
 
\rail@term{oracle}[]
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   406
 
\rail@nont{name}[]
4316
wenzelm
parents: 3213
diff changeset 
   407
 
\rail@term{=}[]
wenzelm
parents: 3213
diff changeset 
   408
 
\rail@nont{name}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   409
 
\rail@end
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   410
 
\rail@begin{1}{ml}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   411
 
\rail@term{ML}[]
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 2657
diff changeset 
   412
 
\rail@nont{text}[]
2657
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   413
 
\rail@end
448bb82c4003 rail output;
wenzelm
parents:
diff changeset 
   414
 
}
isabelle