doc-src/Logics/Sequents.tex
author haftmann
Tue, 13 Jul 2010 11:38:04 +0200
changeset 37788 261c61fabc98
parent 7160 1135f3f8782c
child 42637 381fdcab0f36
permissions -rw-r--r--
corrected title
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7160
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
     1
%% $Id$
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
     2
\chapter{Defining A Sequent-Based Logic}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
     3
\label{chap:sequents}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
     4
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
     5
\underscoreon %this file contains the @ character
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
     6
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
     7
The Isabelle theory \texttt{Sequents.thy} provides facilities for using
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
     8
sequent notation in users' object logics. This theory allows users to
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
     9
easily interface the surface syntax of sequences with an underlying
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    10
representation suitable for higher-order unification.
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    11
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    12
\section{Concrete syntax of sequences}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    13
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    14
Mathematicians and logicians have used sequences in an informal way
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    15
much before proof systems such as Isabelle were created. It seems
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    16
sensible to allow people using Isabelle to express sequents and
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    17
perform proofs in this same informal way, and without requiring the
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    18
theory developer to spend a lot of time in \ML{} programming.
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    19
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    20
By using {\tt Sequents.thy}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    21
appropriately, a logic developer can allow users to refer to sequences
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    22
in several ways:
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    23
%
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    24
\begin{itemize}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    25
\item A sequence variable is any alphanumeric string with the first
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    26
 character being a \verb%$% sign. 
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    27
So, consider the sequent \verb%$A |- B%, where \verb%$A%
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    28
is intended to match a sequence of zero or more items.
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    29
 
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    30
\item A sequence with unspecified sub-sequences and unspecified or
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    31
individual items is written as a comma-separated list of regular
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    32
variables (representing items), particular items, and
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    33
sequence variables, as in  
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    34
\begin{ttbox}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    35
$A, B, C, $D(x) |- E
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    36
\end{ttbox}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    37
Here both \verb%$A% and \verb%$D(x)%
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    38
are allowed to match any subsequences of items on either side of the
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    39
two items that match $B$ and $C$.  Moreover, the sequence matching
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    40
\verb%$D(x)% may contain occurrences of~$x$.
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    41
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    42
\item An empty sequence can be represented by a blank space, as in
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    43
\verb? |- true?.
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    44
\end{itemize}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    45
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    46
These syntactic constructs need to be assimilated into the object
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    47
theory being developed. The type that we use for these visible objects
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    48
is given the name {\tt seq}.
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    49
A {\tt seq} is created either by the empty space, a {\tt seqobj} or a
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    50
{\tt seqobj} followed by a {\tt seq}, with a comma between them. A
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    51
{\tt seqobj} is either an item or a variable representing a
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    52
sequence. Thus, a theory designer can specify a function that takes
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    53
two sequences and returns a meta-level proposition by giving it the
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    54
Isabelle type \verb|[seq, seq] => prop|.
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    55
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    56
This is all part of the concrete syntax, but one may wish to
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    57
exploit Isabelle's higher-order abstract syntax by actually having a
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    58
different, more powerful {\em internal} syntax.
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    59
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    60
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    61
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    62
\section{ Basis}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    63
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    64
One could opt to represent sequences as first-order objects (such as
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    65
simple lists), but this would not allow us to use many facilities
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    66
Isabelle provides for matching.  By using a slightly more complex
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    67
representation, users of the logic can reap many benefits in
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    68
facilities for proofs and ease of reading logical terms.
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    69
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    70
A sequence can be represented as a function --- a constructor for
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    71
further sequences --- by defining a binary {\em abstract} function
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    72
\verb|Seq0'| with type \verb|[o,seq']=>seq'|, and translating a
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    73
sequence such as \verb|A, B, C| into
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    74
\begin{ttbox}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    75
\%s. Seq0'(A, SeqO'(B, SeqO'(C, s)))  
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    76
\end{ttbox}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    77
This sequence can therefore be seen as a constructor 
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    78
for further sequences. The constructor \verb|Seq0'| is never given a
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    79
value, and therefore it is not possible to evaluate this expression
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    80
into a basic value.
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    81
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    82
Furthermore, if we want to represent the sequence \verb|A, $B, C|,
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    83
we note that \verb|$B| already represents a sequence, so we can use
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    84
\verb|B| itself to refer to the function, and therefore the sequence
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    85
can be mapped to the internal form:
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    86
\verb|%s. SeqO'(A, B(SeqO'(C, s)))|.
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    87
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    88
So, while we wish to continue with the standard, well-liked {\em
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    89
external} representation of sequences, we can represent them {\em
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    90
internally} as functions of type \verb|seq'=>seq'|.
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    91
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    92
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    93
\section{Object logics}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    94
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    95
Recall that object logics are defined by mapping elements of
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    96
particular types to the Isabelle type \verb|prop|, usually with a
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    97
function called {\tt Trueprop}. So, an object
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    98
logic proposition {\tt P} is matched to the Isabelle proposition
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
    99
{\tt Trueprop(P)}\@.  The name of the function is often hidden, so the
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   100
user just sees {\tt P}\@. Isabelle is eager to make types match, so it
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   101
inserts {\tt Trueprop} automatically when an object of type {\tt prop}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   102
is expected. This mechanism can be observed in most of the object
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   103
logics which are direct descendants of {\tt Pure}.
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   104
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   105
In order to provide the desired syntactic facilities for sequent
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   106
calculi, rather than use just one function that maps object-level
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   107
propositions to meta-level propositions, we use two functions, and
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   108
separate internal from the external representation. 
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   109
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   110
These functions need to be given a type that is appropriate for the particular
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   111
form of sequents required: single or multiple conclusions.  So
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   112
multiple-conclusion sequents (used in the LK logic) can be
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   113
specified by the following two definitions, which are lifted from the inbuilt
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   114
{\tt Sequents/LK.thy}:
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   115
\begin{ttbox}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   116
 Trueprop       :: two_seqi
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   117
 "@Trueprop"    :: two_seqe   ("((_)/ |- (_))" [6,6] 5)
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   118
\end{ttbox}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   119
%
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   120
where the types used are defined in {\tt Sequents.thy} as
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   121
abbreviations:
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   122
\begin{ttbox}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   123
 two_seqi = [seq'=>seq', seq'=>seq'] => prop
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   124
 two_seqe = [seq, seq] => prop
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   125
\end{ttbox}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   126
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   127
The next step is to actually create links into the low-level parsing
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   128
and pretty-printing mechanisms, which map external and internal
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   129
representations. These functions go below the user level and capture
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   130
the underlying structure of Isabelle terms in \ML{}\@.  Fortunately the
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   131
theory developer need not delve in this level; {\tt Sequents.thy}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   132
provides the necessary facilities. All the theory developer needs to
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   133
add in the \ML{} section is a specification of the two translation
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   134
functions:
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   135
\begin{ttbox}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   136
ML
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   137
val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop")];
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   138
val print_translation = [("Trueprop",Sequents.two_seq_tr' "@Trueprop")];
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   139
\end{ttbox}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   140
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   141
In summary: in the logic theory being developed, the developer needs
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   142
to specify the types for the internal and external representation of
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   143
the sequences, and use the appropriate parsing and pretty-printing
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   144
functions. 
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   145
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   146
\section{What's in \texttt{Sequents.thy}}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   147
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   148
Theory \texttt{Sequents.thy} makes many declarations that you need to know
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   149
about: 
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   150
\begin{enumerate}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   151
\item The Isabelle types given below, which can be used for the
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   152
constants that map object-level sequents and meta-level propositions:
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   153
%
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   154
\begin{ttbox}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   155
 single_seqe = [seq,seqobj] => prop
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   156
 single_seqi = [seq'=>seq',seq'=>seq'] => prop
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   157
 two_seqi    = [seq'=>seq', seq'=>seq'] => prop
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   158
 two_seqe    = [seq, seq] => prop
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   159
 three_seqi  = [seq'=>seq', seq'=>seq', seq'=>seq'] => prop
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   160
 three_seqe  = [seq, seq, seq] => prop
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   161
 four_seqi   = [seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   162
 four_seqe   = [seq, seq, seq, seq] => prop
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   163
\end{ttbox}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   164
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   165
The \verb|single_| and \verb|two_| sets of mappings for internal and
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   166
external representations are the ones used for, say single and
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   167
multiple conclusion sequents. The other functions are provided to
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   168
allow rules that manipulate more than two functions, as can be seen in
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   169
the inbuilt object logics.
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   170
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   171
\item An auxiliary syntactic constant has been
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   172
defined that directly maps a sequence to its internal representation:
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   173
\begin{ttbox}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   174
"@Side"  :: seq=>(seq'=>seq')     ("<<(_)>>")
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   175
\end{ttbox}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   176
Whenever a sequence (such as \verb|<< A, $B, $C>>|) is entered using this
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   177
syntax, it is translated into the appropriate internal representation.  This
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   178
form can be used only where a sequence is expected.
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   179
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   180
\item The \ML{} functions \texttt{single\_tr}, \texttt{two\_seq\_tr},
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   181
  \texttt{three\_seq\_tr}, \texttt{four\_seq\_tr} for parsing, that is, the
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   182
  translation from external to internal form.  Analogously there are
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   183
  \texttt{single\_tr'}, \texttt{two\_seq\_tr'}, \texttt{three\_seq\_tr'},
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   184
  \texttt{four\_seq\_tr'} for pretty-printing, that is, the translation from
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   185
  internal to external form.  These functions can be used in the \ML{} section
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   186
  of a theory file to specify the translations to be used.  As an example of
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   187
  use, note that in {\tt LK.thy} we declare two identifiers:
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   188
\begin{ttbox}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   189
val parse_translation =
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   190
    [("@Trueprop",Sequents.two_seq_tr "Trueprop")];
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   191
val print_translation =
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   192
    [("Trueprop",Sequents.two_seq_tr' "@Trueprop")];
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   193
\end{ttbox}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   194
The given parse translation will be applied whenever a \verb|@Trueprop|
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   195
constant is found, translating using \verb|two_seq_tr| and inserting the
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   196
constant \verb|Trueprop|.  The pretty-printing translation is applied
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   197
analogously; a term that contains \verb|Trueprop| is printed as a
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   198
\verb|@Trueprop|.
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   199
\end{enumerate}
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   200
1135f3f8782c new chapter on Sequents
paulson
parents:
diff changeset
   201