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/HOL/logics-HOL.rao
author wenzelm
Tue, 04 May 1999 18:03:56 +0200
changeset 6580 ff2c3ffd38ee
permissions -rw-r--r--
used to be part of 'logics' manual;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6580
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
     1
 
% This file was generated by 'rail' from 'logics-HOL.rai'
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
     2
 
\rail@i {1}{ typedef : 'typedef' ( () | '(' name ')') type '=' set witness; \par type : typevarlist name ( () | '(' infix ')' ); set : string; witness : () | '(' id ')'; }
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
     3
 
\rail@o {1}{
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
     4
 
\rail@begin{2}{typedef}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
     5
 
\rail@term{typedef}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
     6
 
\rail@bar
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
     7
 
\rail@nextbar{1}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
     8
 
\rail@term{(}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
     9
 
\rail@nont{name}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    10
 
\rail@term{)}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    11
 
\rail@endbar
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    12
 
\rail@nont{type}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    13
 
\rail@term{=}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    14
 
\rail@nont{set}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    15
 
\rail@nont{witness}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    16
 
\rail@end
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    17
 
\rail@begin{2}{type}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    18
 
\rail@nont{typevarlist}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    19
 
\rail@nont{name}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    20
 
\rail@bar
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    21
 
\rail@nextbar{1}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    22
 
\rail@term{(}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    23
 
\rail@nont{infix}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    24
 
\rail@term{)}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    25
 
\rail@endbar
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    26
 
\rail@end
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    27
 
\rail@begin{1}{set}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    28
 
\rail@nont{string}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    29
 
\rail@end
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    30
 
\rail@begin{2}{witness}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    31
 
\rail@bar
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    32
 
\rail@nextbar{1}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    33
 
\rail@term{(}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    34
 
\rail@nont{id}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    35
 
\rail@term{)}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    36
 
\rail@endbar
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    37
 
\rail@end
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    38
 
}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    39
 
\rail@i {2}{ record : 'record' typevarlist name '=' parent (field +); \par parent : ( () | type '+'); field : name '::' type; }
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    40
 
\rail@o {2}{
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    41
 
\rail@begin{2}{record}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    42
 
\rail@term{record}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    43
 
\rail@nont{typevarlist}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    44
 
\rail@nont{name}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    45
 
\rail@term{=}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    46
 
\rail@nont{parent}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    47
 
\rail@plus
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    48
 
\rail@nont{field}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    49
 
\rail@nextplus{1}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    50
 
\rail@endplus
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    51
 
\rail@end
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    52
 
\rail@begin{2}{parent}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    53
 
\rail@bar
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    54
 
\rail@nextbar{1}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    55
 
\rail@nont{type}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    56
 
\rail@term{+}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    57
 
\rail@endbar
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    58
 
\rail@end
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    59
 
\rail@begin{1}{field}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    60
 
\rail@nont{name}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    61
 
\rail@term{::}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    62
 
\rail@nont{type}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    63
 
\rail@end
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    64
 
}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
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 ')') ; }
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    66
 
\rail@o {3}{
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    67
 
\rail@begin{1}{datatype}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    68
 
\rail@term{datatype}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    69
 
\rail@nont{typedecls}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    70
 
\rail@end
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    71
 
\rail@begin{3}{typedecls}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    72
 
\rail@plus
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    73
 
\rail@nont{newtype}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    74
 
\rail@term{=}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    75
 
\rail@plus
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    76
 
\rail@nont{cons}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    77
 
\rail@nextplus{1}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    78
 
\rail@cterm{|}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    79
 
\rail@endplus
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    80
 
\rail@nextplus{2}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    81
 
\rail@cterm{and}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    82
 
\rail@endplus
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    83
 
\rail@end
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    84
 
\rail@begin{2}{newtype}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    85
 
\rail@nont{typevarlist}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    86
 
\rail@nont{id}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    87
 
\rail@bar
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    88
 
\rail@nextbar{1}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    89
 
\rail@term{(}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    90
 
\rail@nont{infix}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    91
 
\rail@term{)}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    92
 
\rail@endbar
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    93
 
\rail@end
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    94
 
\rail@begin{3}{cons}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    95
 
\rail@nont{name}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    96
 
\rail@bar
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    97
 
\rail@nextbar{1}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    98
 
\rail@plus
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
    99
 
\rail@nont{argtype}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
   100
 
\rail@nextplus{2}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
   101
 
\rail@endplus
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
   102
 
\rail@endbar
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
   103
 
\rail@bar
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
   104
 
\rail@nextbar{1}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
   105
 
\rail@term{(}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
   106
 
\rail@nont{mixfix}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
   107
 
\rail@term{)}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
   108
 
\rail@endbar
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
   109
 
\rail@end
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
   110
 
\rail@begin{3}{argtype}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
   111
 
\rail@bar
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
   112
 
\rail@nont{id}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
   113
 
\rail@nextbar{1}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
   114
 
\rail@nont{tid}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
   115
 
\rail@nextbar{2}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
   116
 
\rail@term{(}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
   117
 
\rail@nont{typevarlist}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
   118
 
\rail@nont{id}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
   119
 
\rail@term{)}[]
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
   120
 
\rail@endbar
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
   121
 
\rail@end
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset 
   122
 
}
isabelle