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/Logics/logics.rao
author nipkow
Fri, 27 Nov 1998 16:54:59 +0100
changeset 5982 aeb97860d352
parent 5763 58ed0a78906d
child 6407 ec60d821f3f6
permissions -rw-r--r--
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3150
wenzelm
parents: 3096
diff changeset 
     1
 
% This file was generated by 'rail' from 'logics.rai'
5763
58ed0a78906d *** empty log message ***
wenzelm
parents: 5743
diff changeset 
     2
 
\rail@i {1}{ typedef : 'typedef' ( () | '(' name ')') type '=' set witness; \par type : typevarlist name ( () | '(' infix ')' ); set : string; witness : () | '(' id ')'; }
2660
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
     3
 
\rail@o {1}{
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
     4
 
\rail@begin{2}{typedef}
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2660
diff changeset 
     5
 
\rail@term{typedef}[]
2660
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
     6
 
\rail@bar
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
     7
 
\rail@nextbar{1}
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2660
diff changeset 
     8
 
\rail@term{(}[]
3150
wenzelm
parents: 3096
diff changeset 
     9
 
\rail@nont{name}[]
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2660
diff changeset 
    10
 
\rail@term{)}[]
2660
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
    11
 
\rail@endbar
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2660
diff changeset 
    12
 
\rail@nont{type}[]
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2660
diff changeset 
    13
 
\rail@term{=}[]
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2660
diff changeset 
    14
 
\rail@nont{set}[]
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2660
diff changeset 
    15
 
\rail@nont{witness}[]
2660
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
    16
 
\rail@end
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
    17
 
\rail@begin{2}{type}
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2660
diff changeset 
    18
 
\rail@nont{typevarlist}[]
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2660
diff changeset 
    19
 
\rail@nont{name}[]
2660
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
    20
 
\rail@bar
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
    21
 
\rail@nextbar{1}
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2660
diff changeset 
    22
 
\rail@term{(}[]
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2660
diff changeset 
    23
 
\rail@nont{infix}[]
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2660
diff changeset 
    24
 
\rail@term{)}[]
2660
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
    25
 
\rail@endbar
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
    26
 
\rail@end
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
    27
 
\rail@begin{1}{set}
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2660
diff changeset 
    28
 
\rail@nont{string}[]
2660
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
    29
 
\rail@end
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
    30
 
\rail@begin{2}{witness}
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
    31
 
\rail@bar
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
    32
 
\rail@nextbar{1}
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2660
diff changeset 
    33
 
\rail@term{(}[]
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2660
diff changeset 
    34
 
\rail@nont{id}[]
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2660
diff changeset 
    35
 
\rail@term{)}[]
2660
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
    36
 
\rail@endbar
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
    37
 
\rail@end
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
    38
 
}
5763
58ed0a78906d *** empty log message ***
wenzelm
parents: 5743
diff changeset 
    39
 
\rail@i {2}{ record : 'record' typevarlist name '=' parent (field +); \par parent : ( () | type '+'); field : name '::' type; }
2660
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
    40
 
\rail@o {2}{
5735
6b8bb85c3848 started to add records;
wenzelm
parents: 3150
diff changeset 
    41
 
\rail@begin{2}{record}
6b8bb85c3848 started to add records;
wenzelm
parents: 3150
diff changeset 
    42
 
\rail@term{record}[]
6b8bb85c3848 started to add records;
wenzelm
parents: 3150
diff changeset 
    43
 
\rail@nont{typevarlist}[]
6b8bb85c3848 started to add records;
wenzelm
parents: 3150
diff changeset 
    44
 
\rail@nont{name}[]
6b8bb85c3848 started to add records;
wenzelm
parents: 3150
diff changeset 
    45
 
\rail@term{=}[]
6b8bb85c3848 started to add records;
wenzelm
parents: 3150
diff changeset 
    46
 
\rail@nont{parent}[]
6b8bb85c3848 started to add records;
wenzelm
parents: 3150
diff changeset 
    47
 
\rail@plus
6b8bb85c3848 started to add records;
wenzelm
parents: 3150
diff changeset 
    48
 
\rail@nont{field}[]
6b8bb85c3848 started to add records;
wenzelm
parents: 3150
diff changeset 
    49
 
\rail@nextplus{1}
6b8bb85c3848 started to add records;
wenzelm
parents: 3150
diff changeset 
    50
 
\rail@endplus
6b8bb85c3848 started to add records;
wenzelm
parents: 3150
diff changeset 
    51
 
\rail@end
6b8bb85c3848 started to add records;
wenzelm
parents: 3150
diff changeset 
    52
 
\rail@begin{2}{parent}
6b8bb85c3848 started to add records;
wenzelm
parents: 3150
diff changeset 
    53
 
\rail@bar
6b8bb85c3848 started to add records;
wenzelm
parents: 3150
diff changeset 
    54
 
\rail@nextbar{1}
6b8bb85c3848 started to add records;
wenzelm
parents: 3150
diff changeset 
    55
 
\rail@nont{type}[]
6b8bb85c3848 started to add records;
wenzelm
parents: 3150
diff changeset 
    56
 
\rail@term{+}[]
6b8bb85c3848 started to add records;
wenzelm
parents: 3150
diff changeset 
    57
 
\rail@endbar
6b8bb85c3848 started to add records;
wenzelm
parents: 3150
diff changeset 
    58
 
\rail@end
6b8bb85c3848 started to add records;
wenzelm
parents: 3150
diff changeset 
    59
 
\rail@begin{1}{field}
6b8bb85c3848 started to add records;
wenzelm
parents: 3150
diff changeset 
    60
 
\rail@nont{name}[]
6b8bb85c3848 started to add records;
wenzelm
parents: 3150
diff changeset 
    61
 
\rail@term{::}[]
6b8bb85c3848 started to add records;
wenzelm
parents: 3150
diff changeset 
    62
 
\rail@nont{type}[]
6b8bb85c3848 started to add records;
wenzelm
parents: 3150
diff changeset 
    63
 
\rail@end
6b8bb85c3848 started to add records;
wenzelm
parents: 3150
diff changeset 
    64
 
}
5763
58ed0a78906d *** empty log message ***
wenzelm
parents: 5743
diff changeset 
    65
 
\rail@i {3}{ datatype : 'datatype' typedecls; \par typedecls: ( newtype '=' (cons + '|') ) + 'and' ; newtype : typevarlist id ( () | '(' infix ')' ) ; cons : name (argtype *) ( () | ( '(' mixfix ')' ) ) ; argtype : id | tid | ('(' typevarlist id ')') ; }
5735
6b8bb85c3848 started to add records;
wenzelm
parents: 3150
diff changeset 
    66
 
\rail@o {3}{
5763
58ed0a78906d *** empty log message ***
wenzelm
parents: 5743
diff changeset 
    67
 
\rail@begin{1}{datatype}
58ed0a78906d *** empty log message ***
wenzelm
parents: 5743
diff changeset 
    68
 
\rail@term{datatype}[]
58ed0a78906d *** empty log message ***
wenzelm
parents: 5743
diff changeset 
    69
 
\rail@nont{typedecls}[]
58ed0a78906d *** empty log message ***
wenzelm
parents: 5743
diff changeset 
    70
 
\rail@end
58ed0a78906d *** empty log message ***
wenzelm
parents: 5743
diff changeset 
    71
 
\rail@begin{3}{typedecls}
5743
f2cf404a9579 Updated to new datatype package.
berghofe
parents: 5735
diff changeset 
    72
 
\rail@plus
5763
58ed0a78906d *** empty log message ***
wenzelm
parents: 5743
diff changeset 
    73
 
\rail@nont{newtype}[]
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2660
diff changeset 
    74
 
\rail@term{=}[]
2660
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
    75
 
\rail@plus
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2660
diff changeset 
    76
 
\rail@nont{cons}[]
2660
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
    77
 
\rail@nextplus{1}
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2660
diff changeset 
    78
 
\rail@cterm{|}[]
2660
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
    79
 
\rail@endplus
5743
f2cf404a9579 Updated to new datatype package.
berghofe
parents: 5735
diff changeset 
    80
 
\rail@nextplus{2}
f2cf404a9579 Updated to new datatype package.
berghofe
parents: 5735
diff changeset 
    81
 
\rail@cterm{and}[]
f2cf404a9579 Updated to new datatype package.
berghofe
parents: 5735
diff changeset 
    82
 
\rail@endplus
f2cf404a9579 Updated to new datatype package.
berghofe
parents: 5735
diff changeset 
    83
 
\rail@end
5763
58ed0a78906d *** empty log message ***
wenzelm
parents: 5743
diff changeset 
    84
 
\rail@begin{2}{newtype}
5743
f2cf404a9579 Updated to new datatype package.
berghofe
parents: 5735
diff changeset 
    85
 
\rail@nont{typevarlist}[]
f2cf404a9579 Updated to new datatype package.
berghofe
parents: 5735
diff changeset 
    86
 
\rail@nont{id}[]
f2cf404a9579 Updated to new datatype package.
berghofe
parents: 5735
diff changeset 
    87
 
\rail@bar
f2cf404a9579 Updated to new datatype package.
berghofe
parents: 5735
diff changeset 
    88
 
\rail@nextbar{1}
f2cf404a9579 Updated to new datatype package.
berghofe
parents: 5735
diff changeset 
    89
 
\rail@term{(}[]
f2cf404a9579 Updated to new datatype package.
berghofe
parents: 5735
diff changeset 
    90
 
\rail@nont{infix}[]
f2cf404a9579 Updated to new datatype package.
berghofe
parents: 5735
diff changeset 
    91
 
\rail@term{)}[]
f2cf404a9579 Updated to new datatype package.
berghofe
parents: 5735
diff changeset 
    92
 
\rail@endbar
2660
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
    93
 
\rail@end
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
    94
 
\rail@begin{3}{cons}
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2660
diff changeset 
    95
 
\rail@nont{name}[]
2660
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
    96
 
\rail@bar
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
    97
 
\rail@nextbar{1}
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
    98
 
\rail@plus
5743
f2cf404a9579 Updated to new datatype package.
berghofe
parents: 5735
diff changeset 
    99
 
\rail@nont{argtype}[]
2660
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
   100
 
\rail@nextplus{2}
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
   101
 
\rail@endplus
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
   102
 
\rail@endbar
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
   103
 
\rail@bar
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
   104
 
\rail@nextbar{1}
5743
f2cf404a9579 Updated to new datatype package.
berghofe
parents: 5735
diff changeset 
   105
 
\rail@term{(}[]
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2660
diff changeset 
   106
 
\rail@nont{mixfix}[]
5743
f2cf404a9579 Updated to new datatype package.
berghofe
parents: 5735
diff changeset 
   107
 
\rail@term{)}[]
2660
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
   108
 
\rail@endbar
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
   109
 
\rail@end
5743
f2cf404a9579 Updated to new datatype package.
berghofe
parents: 5735
diff changeset 
   110
 
\rail@begin{3}{argtype}
2660
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
   111
 
\rail@bar
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2660
diff changeset 
   112
 
\rail@nont{id}[]
2660
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
   113
 
\rail@nextbar{1}
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2660
diff changeset 
   114
 
\rail@nont{tid}[]
2660
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
   115
 
\rail@nextbar{2}
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2660
diff changeset 
   116
 
\rail@term{(}[]
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2660
diff changeset 
   117
 
\rail@nont{typevarlist}[]
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2660
diff changeset 
   118
 
\rail@nont{id}[]
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2660
diff changeset 
   119
 
\rail@term{)}[]
2660
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
   120
 
\rail@endbar
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
   121
 
\rail@end
9137a3d10d57 rail output;
wenzelm
parents:
diff changeset 
   122
 
}
isabelle