doc-src/IsarImplementation/Thy/document/logic.tex
author wenzelm
Mon, 04 Sep 2006 16:28:36 +0200
changeset 20471 ffafbd4103c0
parent 20451 27ea2ba48fa3
child 20472 e993073eda4c
permissions -rw-r--r--
updated;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     1
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     2
\begin{isabellebody}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     3
\def\isabellecontext{logic}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     4
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     5
\isadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     6
\isanewline
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     7
\isanewline
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     8
\isanewline
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     9
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    10
\endisadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    11
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    12
\isatagtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    13
\isacommand{theory}\isamarkupfalse%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    14
\ logic\ \isakeyword{imports}\ base\ \isakeyword{begin}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    15
\endisatagtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    16
{\isafoldtheory}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    17
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    18
\isadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    19
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    20
\endisadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    21
%
20471
ffafbd4103c0 updated;
wenzelm
parents: 20451
diff changeset
    22
\isamarkupchapter{Primitive logic \label{ch:logic}%
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    23
}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    24
\isamarkuptrue%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    25
%
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    26
\isamarkupsection{Variable names%
20438
9060c73a4578 updated;
wenzelm
parents: 18537
diff changeset
    27
}
9060c73a4578 updated;
wenzelm
parents: 18537
diff changeset
    28
\isamarkuptrue%
9060c73a4578 updated;
wenzelm
parents: 18537
diff changeset
    29
%
9060c73a4578 updated;
wenzelm
parents: 18537
diff changeset
    30
\begin{isamarkuptext}%
9060c73a4578 updated;
wenzelm
parents: 18537
diff changeset
    31
FIXME%
9060c73a4578 updated;
wenzelm
parents: 18537
diff changeset
    32
\end{isamarkuptext}%
9060c73a4578 updated;
wenzelm
parents: 18537
diff changeset
    33
\isamarkuptrue%
9060c73a4578 updated;
wenzelm
parents: 18537
diff changeset
    34
%
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    35
\isamarkupsection{Types \label{sec:types}%
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    36
}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    37
\isamarkuptrue%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    38
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    39
\begin{isamarkuptext}%
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    40
\glossary{Type class}{FIXME}
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    41
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    42
  \glossary{Type arity}{FIXME}
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    43
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    44
  \glossary{Sort}{FIXME}
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    45
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    46
  FIXME classes and sorts
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    47
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    48
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    49
  \glossary{Type}{FIXME}
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    50
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    51
  \glossary{Type constructor}{FIXME}
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    52
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    53
  \glossary{Type variable}{FIXME}
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    54
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    55
  FIXME simple types%
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    56
\end{isamarkuptext}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    57
\isamarkuptrue%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    58
%
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    59
\isamarkupsection{Terms \label{sec:terms}%
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    60
}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    61
\isamarkuptrue%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    62
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    63
\begin{isamarkuptext}%
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    64
\glossary{Term}{FIXME}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    65
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    66
  FIXME de-Bruijn representation of lambda terms%
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    67
\end{isamarkuptext}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    68
\isamarkuptrue%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    69
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    70
\begin{isamarkuptext}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    71
FIXME
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    72
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    73
\glossary{Schematic polymorphism}{FIXME}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    74
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    75
\glossary{Type variable}{FIXME}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    76
\end{isamarkuptext}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    77
\isamarkuptrue%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    78
%
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    79
\isamarkupsection{Theorems \label{sec:thms}%
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    80
}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    81
\isamarkuptrue%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    82
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    83
\begin{isamarkuptext}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    84
FIXME
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    85
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    86
\glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    87
\isa{prop}.  Internally, there is nothing special about
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    88
propositions apart from their type, but the concrete syntax enforces a
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    89
clear distinction.  Propositions are structured via implication \isa{A\ {\isasymLongrightarrow}\ B} or universal quantification \isa{{\isasymAnd}x{\isachardot}\ B\ x} --- anything
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    90
else is considered atomic.  The canonical form for propositions is
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    91
that of a \seeglossary{Hereditary Harrop Formula}.}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    92
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    93
\glossary{Theorem}{A proven proposition within a certain theory and
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    94
proof context, formally \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}; both contexts are
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    95
rarely spelled out explicitly.  Theorems are usually normalized
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    96
according to the \seeglossary{HHF} format.}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    97
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    98
\glossary{Fact}{Sometimes used interchangably for
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    99
\seeglossary{theorem}.  Strictly speaking, a list of theorems,
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   100
essentially an extra-logical conjunction.  Facts emerge either as
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   101
local assumptions, or as results of local goal statements --- both may
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   102
be simultaneous, hence the list representation.}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   103
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   104
\glossary{Schematic variable}{FIXME}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   105
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   106
\glossary{Fixed variable}{A variable that is bound within a certain
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   107
proof context; an arbitrary-but-fixed entity within a portion of proof
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   108
text.}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   109
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   110
\glossary{Free variable}{Synonymous for \seeglossary{fixed variable}.}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   111
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   112
\glossary{Bound variable}{FIXME}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   113
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   114
\glossary{Variable}{See \seeglossary{schematic variable},
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   115
\seeglossary{fixed variable}, \seeglossary{bound variable}, or
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   116
\seeglossary{type variable}.  The distinguishing feature of different
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   117
variables is their binding scope.}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   118
\end{isamarkuptext}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   119
\isamarkuptrue%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   120
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   121
\isamarkupsubsection{Primitive inferences%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   122
}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   123
\isamarkuptrue%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   124
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   125
\begin{isamarkuptext}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   126
FIXME%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   127
\end{isamarkuptext}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   128
\isamarkuptrue%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   129
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   130
\isamarkupsubsection{Higher-order resolution%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   131
}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   132
\isamarkuptrue%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   133
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   134
\begin{isamarkuptext}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   135
FIXME
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   136
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   137
\glossary{Hereditary Harrop Formula}{The set of propositions in HHF
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   138
format is defined inductively as \isa{H\ {\isacharequal}\ {\isacharparenleft}{\isasymAnd}x\isactrlsup {\isacharasterisk}{\isachardot}\ H\isactrlsup {\isacharasterisk}\ {\isasymLongrightarrow}\ A{\isacharparenright}}, for variables \isa{x} and atomic propositions \isa{A}.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   139
Any proposition may be put into HHF form by normalizing with the rule
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   140
\isa{{\isacharparenleft}A\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ B\ x{\isacharparenright}{\isacharparenright}\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ A\ {\isasymLongrightarrow}\ B\ x{\isacharparenright}}.  In Isabelle, the outermost
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   141
quantifier prefix is represented via \seeglossary{schematic
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   142
variables}, such that the top-level structure is merely that of a
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   143
\seeglossary{Horn Clause}}.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   144
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   145
\glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   146
\end{isamarkuptext}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   147
\isamarkuptrue%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   148
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   149
\isamarkupsubsection{Equational reasoning%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   150
}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   151
\isamarkuptrue%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   152
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   153
\begin{isamarkuptext}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   154
FIXME%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   155
\end{isamarkuptext}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   156
\isamarkuptrue%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   157
%
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
   158
\isamarkupsection{Low-level specifications%
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   159
}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   160
\isamarkuptrue%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   161
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   162
\begin{isamarkuptext}%
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
   163
FIXME
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
   164
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
   165
\glossary{Constant}{Essentially a \seeglossary{fixed variable} of the
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
   166
theory context, but slightly more flexible since it may be used at
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
   167
different type-instances, due to \seeglossary{schematic
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
   168
polymorphism.}}
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
   169
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
   170
\glossary{Axiom}{FIXME}
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
   171
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
   172
\glossary{Primitive definition}{FIXME}%
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   173
\end{isamarkuptext}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   174
\isamarkuptrue%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   175
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   176
\isadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   177
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   178
\endisadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   179
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   180
\isatagtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   181
\isacommand{end}\isamarkupfalse%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   182
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   183
\endisatagtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   184
{\isafoldtheory}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   185
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   186
\isadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   187
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   188
\endisadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   189
\isanewline
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   190
\end{isabellebody}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   191
%%% Local Variables:
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   192
%%% mode: latex
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   193
%%% TeX-master: "root"
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   194
%%% End: