1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Nov 13 21:41:04 2008 +0100
1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Nov 13 21:43:46 2008 +0100
1.3 @@ -28,19 +28,19 @@
1.4 ;
1.5 \end{rail}
1.6
1.7 - \begin{descr}
1.8 + \begin{description}
1.9
1.10 - \item [@{command (HOL) "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n)
1.11 - t"}] is similar to the original @{command "typedecl"} of
1.12 - Isabelle/Pure (see \secref{sec:types-pure}), but also declares type
1.13 - arity @{text "t :: (type, \<dots>, type) type"}, making @{text t} an
1.14 - actual HOL type constructor. %FIXME check, update
1.15 + \item @{command (HOL) "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} is similar
1.16 + to the original @{command "typedecl"} of Isabelle/Pure (see
1.17 + \secref{sec:types-pure}), but also declares type arity @{text "t ::
1.18 + (type, \<dots>, type) type"}, making @{text t} an actual HOL type
1.19 + constructor. %FIXME check, update
1.20
1.21 - \item [@{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n)
1.22 - t = A"}] sets up a goal stating non-emptiness of the set @{text A}.
1.23 - After finishing the proof, the theory will be augmented by a
1.24 - Gordon/HOL-style type definition, which establishes a bijection
1.25 - between the representing set @{text A} and the new type @{text t}.
1.26 + \item @{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A"} sets up
1.27 + a goal stating non-emptiness of the set @{text A}. After finishing
1.28 + the proof, the theory will be augmented by a Gordon/HOL-style type
1.29 + definition, which establishes a bijection between the representing
1.30 + set @{text A} and the new type @{text t}.
1.31
1.32 Technically, @{command (HOL) "typedef"} defines both a type @{text
1.33 t} and a set (term constant) of the same name (an alternative base
1.34 @@ -64,7 +64,7 @@
1.35 declaration suppresses a separate constant definition for the
1.36 representing set.
1.37
1.38 - \end{descr}
1.39 + \end{description}
1.40
1.41 Note that raw type declarations are rarely used in practice; the
1.42 main application is with experimental (or even axiomatic!) theory
1.43 @@ -87,21 +87,20 @@
1.44 ;
1.45 \end{rail}
1.46
1.47 - \begin{descr}
1.48 + \begin{description}
1.49
1.50 - \item [@{attribute (HOL) split_format}~@{text "p\<^sub>1 \<dots> p\<^sub>m
1.51 - \<AND> \<dots> \<AND> q\<^sub>1 \<dots> q\<^sub>n"}] puts expressions of
1.52 - low-level tuple types into canonical form as specified by the
1.53 - arguments given; the @{text i}-th collection of arguments refers to
1.54 - occurrences in premise @{text i} of the rule. The ``@{text
1.55 - "(complete)"}'' option causes \emph{all} arguments in function
1.56 - applications to be represented canonically according to their tuple
1.57 - type structure.
1.58 + \item @{attribute (HOL) split_format}~@{text "p\<^sub>1 \<dots> p\<^sub>m \<AND> \<dots>
1.59 + \<AND> q\<^sub>1 \<dots> q\<^sub>n"} puts expressions of low-level tuple types into
1.60 + canonical form as specified by the arguments given; the @{text i}-th
1.61 + collection of arguments refers to occurrences in premise @{text i}
1.62 + of the rule. The ``@{text "(complete)"}'' option causes \emph{all}
1.63 + arguments in function applications to be represented canonically
1.64 + according to their tuple type structure.
1.65
1.66 Note that these operations tend to invent funny names for new local
1.67 parameters to be introduced.
1.68
1.69 - \end{descr}
1.70 + \end{description}
1.71 *}
1.72
1.73
1.74 @@ -194,11 +193,10 @@
1.75 ;
1.76 \end{rail}
1.77
1.78 - \begin{descr}
1.79 + \begin{description}
1.80
1.81 - \item [@{command (HOL) "record"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t
1.82 - = \<tau> + c\<^sub>1 :: \<sigma>\<^sub>1 \<dots> c\<^sub>n :: \<sigma>\<^sub>n"}] defines
1.83 - extensible record type @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"},
1.84 + \item @{command (HOL) "record"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t = \<tau> + c\<^sub>1 :: \<sigma>\<^sub>1
1.85 + \<dots> c\<^sub>n :: \<sigma>\<^sub>n"} defines extensible record type @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"},
1.86 derived from the optional parent record @{text "\<tau>"} by adding new
1.87 field components @{text "c\<^sub>i :: \<sigma>\<^sub>i"} etc.
1.88
1.89 @@ -224,7 +222,7 @@
1.90 @{text "\<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> ::
1.91 \<zeta>\<rparr>"}.
1.92
1.93 - \end{descr}
1.94 + \end{description}
1.95 *}
1.96
1.97
1.98 @@ -376,16 +374,16 @@
1.99 cons: name (type *) mixfix?
1.100 \end{rail}
1.101
1.102 - \begin{descr}
1.103 + \begin{description}
1.104
1.105 - \item [@{command (HOL) "datatype"}] defines inductive datatypes in
1.106 + \item @{command (HOL) "datatype"} defines inductive datatypes in
1.107 HOL.
1.108
1.109 - \item [@{command (HOL) "rep_datatype"}] represents existing types as
1.110 + \item @{command (HOL) "rep_datatype"} represents existing types as
1.111 inductive ones, generating the standard infrastructure of derived
1.112 concepts (primitive recursion etc.).
1.113
1.114 - \end{descr}
1.115 + \end{description}
1.116
1.117 The induction and exhaustion theorems generated provide case names
1.118 according to the constructors involved, while parameters are named
1.119 @@ -425,12 +423,12 @@
1.120 'termination' ( term )?
1.121 \end{rail}
1.122
1.123 - \begin{descr}
1.124 + \begin{description}
1.125
1.126 - \item [@{command (HOL) "primrec"}] defines primitive recursive
1.127 + \item @{command (HOL) "primrec"} defines primitive recursive
1.128 functions over datatypes, see also \cite{isabelle-HOL}.
1.129
1.130 - \item [@{command (HOL) "function"}] defines functions by general
1.131 + \item @{command (HOL) "function"} defines functions by general
1.132 wellfounded recursion. A detailed description with examples can be
1.133 found in \cite{isabelle-function}. The function is specified by a
1.134 set of (possibly conditional) recursive equations with arbitrary
1.135 @@ -443,18 +441,18 @@
1.136 predicate @{text "f_dom"}. The @{command (HOL) "termination"}
1.137 command can then be used to establish that the function is total.
1.138
1.139 - \item [@{command (HOL) "fun"}] is a shorthand notation for
1.140 - ``@{command (HOL) "function"}~@{text "(sequential)"}, followed by
1.141 - automated proof attempts regarding pattern matching and termination.
1.142 - See \cite{isabelle-function} for further details.
1.143 + \item @{command (HOL) "fun"} is a shorthand notation for ``@{command
1.144 + (HOL) "function"}~@{text "(sequential)"}, followed by automated
1.145 + proof attempts regarding pattern matching and termination. See
1.146 + \cite{isabelle-function} for further details.
1.147
1.148 - \item [@{command (HOL) "termination"}~@{text f}] commences a
1.149 + \item @{command (HOL) "termination"}~@{text f} commences a
1.150 termination proof for the previously defined function @{text f}. If
1.151 this is omitted, the command refers to the most recent function
1.152 definition. After the proof is closed, the recursive equations and
1.153 the induction principle is established.
1.154
1.155 - \end{descr}
1.156 + \end{description}
1.157
1.158 %FIXME check
1.159
1.160 @@ -479,31 +477,31 @@
1.161 The @{command (HOL) "function"} command accepts the following
1.162 options.
1.163
1.164 - \begin{descr}
1.165 + \begin{description}
1.166
1.167 - \item [@{text sequential}] enables a preprocessor which
1.168 - disambiguates overlapping patterns by making them mutually disjoint.
1.169 - Earlier equations take precedence over later ones. This allows to
1.170 - give the specification in a format very similar to functional
1.171 - programming. Note that the resulting simplification and induction
1.172 - rules correspond to the transformed specification, not the one given
1.173 + \item @{text sequential} enables a preprocessor which disambiguates
1.174 + overlapping patterns by making them mutually disjoint. Earlier
1.175 + equations take precedence over later ones. This allows to give the
1.176 + specification in a format very similar to functional programming.
1.177 + Note that the resulting simplification and induction rules
1.178 + correspond to the transformed specification, not the one given
1.179 originally. This usually means that each equation given by the user
1.180 may result in several theroems. Also note that this automatic
1.181 transformation only works for ML-style datatype patterns.
1.182
1.183 - \item [@{text domintros}] enables the automated generation of
1.184 + \item @{text domintros} enables the automated generation of
1.185 introduction rules for the domain predicate. While mostly not
1.186 needed, they can be helpful in some proofs about partial functions.
1.187
1.188 - \item [@{text tailrec}] generates the unconstrained recursive
1.189 + \item @{text tailrec} generates the unconstrained recursive
1.190 equations even without a termination proof, provided that the
1.191 function is tail-recursive. This currently only works
1.192
1.193 - \item [@{text "default d"}] allows to specify a default value for a
1.194 + \item @{text "default d"} allows to specify a default value for a
1.195 (partial) function, which will ensure that @{text "f x = d x"}
1.196 whenever @{text "x \<notin> f_dom"}.
1.197
1.198 - \end{descr}
1.199 + \end{description}
1.200 *}
1.201
1.202
1.203 @@ -523,21 +521,21 @@
1.204 ;
1.205 \end{rail}
1.206
1.207 - \begin{descr}
1.208 + \begin{description}
1.209
1.210 - \item [@{method (HOL) pat_completeness}] is a specialized method to
1.211 + \item @{method (HOL) pat_completeness} is a specialized method to
1.212 solve goals regarding the completeness of pattern matching, as
1.213 required by the @{command (HOL) "function"} package (cf.\
1.214 \cite{isabelle-function}).
1.215
1.216 - \item [@{method (HOL) relation}~@{text R}] introduces a termination
1.217 + \item @{method (HOL) relation}~@{text R} introduces a termination
1.218 proof using the relation @{text R}. The resulting proof state will
1.219 contain goals expressing that @{text R} is wellfounded, and that the
1.220 arguments of recursive calls decrease with respect to @{text R}.
1.221 Usually, this method is used as the initial proof step of manual
1.222 termination proofs.
1.223
1.224 - \item [@{method (HOL) "lexicographic_order"}] attempts a fully
1.225 + \item @{method (HOL) "lexicographic_order"} attempts a fully
1.226 automated termination proof by searching for a lexicographic
1.227 combination of size measures on the arguments of the function. The
1.228 method accepts the same arguments as the @{method auto} method,
1.229 @@ -548,7 +546,7 @@
1.230 In case of failure, extensive information is printed, which can help
1.231 to analyse the situation (cf.\ \cite{isabelle-function}).
1.232
1.233 - \end{descr}
1.234 + \end{description}
1.235 *}
1.236
1.237
1.238 @@ -577,9 +575,9 @@
1.239 ;
1.240 \end{rail}
1.241
1.242 - \begin{descr}
1.243 + \begin{description}
1.244
1.245 - \item [@{command (HOL) "recdef"}] defines general well-founded
1.246 + \item @{command (HOL) "recdef"} defines general well-founded
1.247 recursive functions (using the TFL package), see also
1.248 \cite{isabelle-HOL}. The ``@{text "(permissive)"}'' option tells
1.249 TFL to recover from failed proof attempts, returning unfinished
1.250 @@ -590,7 +588,7 @@
1.251 context of the Simplifier (cf.\ \secref{sec:simplifier}) and
1.252 Classical reasoner (cf.\ \secref{sec:classical}).
1.253
1.254 - \item [@{command (HOL) "recdef_tc"}~@{text "c (i)"}] recommences the
1.255 + \item @{command (HOL) "recdef_tc"}~@{text "c (i)"} recommences the
1.256 proof for leftover termination condition number @{text i} (default
1.257 1) as generated by a @{command (HOL) "recdef"} definition of
1.258 constant @{text c}.
1.259 @@ -598,7 +596,7 @@
1.260 Note that in most cases, @{command (HOL) "recdef"} is able to finish
1.261 its internal proofs without manual intervention.
1.262
1.263 - \end{descr}
1.264 + \end{description}
1.265
1.266 \medskip Hints for @{command (HOL) "recdef"} may be also declared
1.267 globally, using the following attributes.
1.268 @@ -659,10 +657,10 @@
1.269 ;
1.270 \end{rail}
1.271
1.272 - \begin{descr}
1.273 + \begin{description}
1.274
1.275 - \item [@{command (HOL) "inductive"} and @{command (HOL)
1.276 - "coinductive"}] define (co)inductive predicates from the
1.277 + \item @{command (HOL) "inductive"} and @{command (HOL)
1.278 + "coinductive"} define (co)inductive predicates from the
1.279 introduction rules given in the @{keyword "where"} part. The
1.280 optional @{keyword "for"} part contains a list of parameters of the
1.281 (co)inductive predicates that remain fixed throughout the
1.282 @@ -672,15 +670,15 @@
1.283 \emph{must} be a theorem of the form @{text "A \<le> B \<Longrightarrow> M A \<le> M B"},
1.284 for each premise @{text "M R\<^sub>i t"} in an introduction rule!
1.285
1.286 - \item [@{command (HOL) "inductive_set"} and @{command (HOL)
1.287 - "coinductive_set"}] are wrappers for to the previous commands,
1.288 + \item @{command (HOL) "inductive_set"} and @{command (HOL)
1.289 + "coinductive_set"} are wrappers for to the previous commands,
1.290 allowing the definition of (co)inductive sets.
1.291
1.292 - \item [@{attribute (HOL) mono}] declares monotonicity rules. These
1.293 + \item @{attribute (HOL) mono} declares monotonicity rules. These
1.294 rule are involved in the automated monotonicity proof of @{command
1.295 (HOL) "inductive"}.
1.296
1.297 - \end{descr}
1.298 + \end{description}
1.299 *}
1.300
1.301
1.302 @@ -692,14 +690,14 @@
1.303
1.304 \begin{description}
1.305
1.306 - \item [@{text R.intros}] is the list of introduction rules as proven
1.307 + \item @{text R.intros} is the list of introduction rules as proven
1.308 theorems, for the recursive predicates (or sets). The rules are
1.309 also available individually, using the names given them in the
1.310 theory file;
1.311
1.312 - \item [@{text R.cases}] is the case analysis (or elimination) rule;
1.313 + \item @{text R.cases} is the case analysis (or elimination) rule;
1.314
1.315 - \item [@{text R.induct} or @{text R.coinduct}] is the (co)induction
1.316 + \item @{text R.induct} or @{text R.coinduct} is the (co)induction
1.317 rule.
1.318
1.319 \end{description}
1.320 @@ -817,13 +815,12 @@
1.321 ;
1.322 \end{rail}
1.323
1.324 - \begin{descr}
1.325 + \begin{description}
1.326
1.327 - \item [@{command (HOL) sledgehammer}~@{text "prover\<^sub>1 \<dots>
1.328 - prover\<^sub>n"}] invokes the specified automated theorem provers on
1.329 - the first subgoal. Provers are run in parallel, the first
1.330 - successful result is displayed, and the other attempts are
1.331 - terminated.
1.332 + \item @{command (HOL) sledgehammer}~@{text "prover\<^sub>1 \<dots> prover\<^sub>n"}
1.333 + invokes the specified automated theorem provers on the first
1.334 + subgoal. Provers are run in parallel, the first successful result
1.335 + is displayed, and the other attempts are terminated.
1.336
1.337 Provers are defined in the theory context, see also @{command (HOL)
1.338 print_atps}. If no provers are given as arguments to @{command
1.339 @@ -834,28 +831,28 @@
1.340 and the maximum number of independent prover processes (default: 5);
1.341 excessive provers are automatically terminated.
1.342
1.343 - \item [@{command (HOL) print_atps}] prints the list of automated
1.344 + \item @{command (HOL) print_atps} prints the list of automated
1.345 theorem provers available to the @{command (HOL) sledgehammer}
1.346 command.
1.347
1.348 - \item [@{command (HOL) atp_info}] prints information about presently
1.349 + \item @{command (HOL) atp_info} prints information about presently
1.350 running provers, including elapsed runtime, and the remaining time
1.351 until timeout.
1.352
1.353 - \item [@{command (HOL) atp_kill}] terminates all presently running
1.354 + \item @{command (HOL) atp_kill} terminates all presently running
1.355 provers.
1.356
1.357 - \item [@{method (HOL) metis}~@{text "facts"}] invokes the Metis
1.358 - prover with the given facts. Metis is an automated proof tool of
1.359 - medium strength, but is fully integrated into Isabelle/HOL, with
1.360 - explicit inferences going through the kernel. Thus its results are
1.361 + \item @{method (HOL) metis}~@{text "facts"} invokes the Metis prover
1.362 + with the given facts. Metis is an automated proof tool of medium
1.363 + strength, but is fully integrated into Isabelle/HOL, with explicit
1.364 + inferences going through the kernel. Thus its results are
1.365 guaranteed to be ``correct by construction''.
1.366
1.367 Note that all facts used with Metis need to be specified as explicit
1.368 arguments. There are no rule declarations as for other Isabelle
1.369 provers, like @{method blast} or @{method fast}.
1.370
1.371 - \end{descr}
1.372 + \end{description}
1.373 *}
1.374
1.375
1.376 @@ -887,13 +884,13 @@
1.377 ;
1.378 \end{rail}
1.379
1.380 - \begin{descr}
1.381 + \begin{description}
1.382
1.383 - \item [@{method (HOL) case_tac} and @{method (HOL) induct_tac}]
1.384 - admit to reason about inductive types. Rules are selected according
1.385 - to the declarations by the @{attribute cases} and @{attribute
1.386 - induct} attributes, cf.\ \secref{sec:cases-induct}. The @{command
1.387 - (HOL) datatype} package already takes care of this.
1.388 + \item @{method (HOL) case_tac} and @{method (HOL) induct_tac} admit
1.389 + to reason about inductive types. Rules are selected according to
1.390 + the declarations by the @{attribute cases} and @{attribute induct}
1.391 + attributes, cf.\ \secref{sec:cases-induct}. The @{command (HOL)
1.392 + datatype} package already takes care of this.
1.393
1.394 These unstructured tactics feature both goal addressing and dynamic
1.395 instantiation. Note that named rule cases are \emph{not} provided
1.396 @@ -903,8 +900,8 @@
1.397 statements, only the compact object-logic conclusion of the subgoal
1.398 being addressed.
1.399
1.400 - \item [@{method (HOL) ind_cases} and @{command (HOL)
1.401 - "inductive_cases"}] provide an interface to the internal @{ML_text
1.402 + \item @{method (HOL) ind_cases} and @{command (HOL)
1.403 + "inductive_cases"} provide an interface to the internal @{ML_text
1.404 mk_cases} operation. Rules are simplified in an unrestricted
1.405 forward manner.
1.406
1.407 @@ -915,7 +912,7 @@
1.408 ind_cases} method allows to specify a list of variables that should
1.409 be generalized before applying the resulting rule.
1.410
1.411 - \end{descr}
1.412 + \end{description}
1.413 *}
1.414
1.415
1.416 @@ -977,12 +974,12 @@
1.417 ;
1.418 \end{rail}
1.419
1.420 - \begin{descr}
1.421 + \begin{description}
1.422
1.423 - \item [@{command (HOL) "value"}~@{text t}] evaluates and prints a
1.424 - term using the code generator.
1.425 + \item @{command (HOL) "value"}~@{text t} evaluates and prints a term
1.426 + using the code generator.
1.427
1.428 - \end{descr}
1.429 + \end{description}
1.430
1.431 \medskip The other framework generates code from functional programs
1.432 (including overloading using type classes) to SML \cite{SML}, OCaml
1.433 @@ -1079,14 +1076,14 @@
1.434 ;
1.435 \end{rail}
1.436
1.437 - \begin{descr}
1.438 + \begin{description}
1.439
1.440 - \item [@{command (HOL) "export_code"}] is the canonical interface
1.441 - for generating and serializing code: for a given list of constants,
1.442 - code is generated for the specified target languages. Abstract code
1.443 - is cached incrementally. If no constant is given, the currently
1.444 - cached code is serialized. If no serialization instruction is
1.445 - given, only abstract code is cached.
1.446 + \item @{command (HOL) "export_code"} is the canonical interface for
1.447 + generating and serializing code: for a given list of constants, code
1.448 + is generated for the specified target languages. Abstract code is
1.449 + cached incrementally. If no constant is given, the currently cached
1.450 + code is serialized. If no serialization instruction is given, only
1.451 + abstract code is cached.
1.452
1.453 Constants may be specified by giving them literally, referring to
1.454 all executable contants within a certain theory by giving @{text
1.455 @@ -1111,71 +1108,70 @@
1.456 "deriving (Read, Show)"}'' clause to each appropriate datatype
1.457 declaration.
1.458
1.459 - \item [@{command (HOL) "code_thms"}] prints a list of theorems
1.460 + \item @{command (HOL) "code_thms"} prints a list of theorems
1.461 representing the corresponding program containing all given
1.462 constants; if no constants are given, the currently cached code
1.463 theorems are printed.
1.464
1.465 - \item [@{command (HOL) "code_deps"}] visualizes dependencies of
1.466 + \item @{command (HOL) "code_deps"} visualizes dependencies of
1.467 theorems representing the corresponding program containing all given
1.468 constants; if no constants are given, the currently cached code
1.469 theorems are visualized.
1.470
1.471 - \item [@{command (HOL) "code_datatype"}] specifies a constructor set
1.472 + \item @{command (HOL) "code_datatype"} specifies a constructor set
1.473 for a logical type.
1.474
1.475 - \item [@{command (HOL) "code_const"}] associates a list of constants
1.476 + \item @{command (HOL) "code_const"} associates a list of constants
1.477 with target-specific serializations; omitting a serialization
1.478 deletes an existing serialization.
1.479
1.480 - \item [@{command (HOL) "code_type"}] associates a list of type
1.481 + \item @{command (HOL) "code_type"} associates a list of type
1.482 constructors with target-specific serializations; omitting a
1.483 serialization deletes an existing serialization.
1.484
1.485 - \item [@{command (HOL) "code_class"}] associates a list of classes
1.486 - with target-specific class names; omitting a
1.487 - serialization deletes an existing serialization.
1.488 - This applies only to \emph{Haskell}.
1.489 + \item @{command (HOL) "code_class"} associates a list of classes
1.490 + with target-specific class names; omitting a serialization deletes
1.491 + an existing serialization. This applies only to \emph{Haskell}.
1.492
1.493 - \item [@{command (HOL) "code_instance"}] declares a list of type
1.494 + \item @{command (HOL) "code_instance"} declares a list of type
1.495 constructor / class instance relations as ``already present'' for a
1.496 given target. Omitting a ``@{text "-"}'' deletes an existing
1.497 ``already present'' declaration. This applies only to
1.498 \emph{Haskell}.
1.499
1.500 - \item [@{command (HOL) "code_monad"}] provides an auxiliary
1.501 - mechanism to generate monadic code for Haskell.
1.502 + \item @{command (HOL) "code_monad"} provides an auxiliary mechanism
1.503 + to generate monadic code for Haskell.
1.504
1.505 - \item [@{command (HOL) "code_reserved"}] declares a list of names as
1.506 + \item @{command (HOL) "code_reserved"} declares a list of names as
1.507 reserved for a given target, preventing it to be shadowed by any
1.508 generated code.
1.509
1.510 - \item [@{command (HOL) "code_include"}] adds arbitrary named content
1.511 + \item @{command (HOL) "code_include"} adds arbitrary named content
1.512 (``include'') to generated code. A ``@{text "-"}'' as last argument
1.513 will remove an already added ``include''.
1.514
1.515 - \item [@{command (HOL) "code_modulename"}] declares aliasings from
1.516 - one module name onto another.
1.517 + \item @{command (HOL) "code_modulename"} declares aliasings from one
1.518 + module name onto another.
1.519
1.520 - \item [@{command (HOL) "code_abort"}] declares constants which
1.521 - are not required to have a definition by means of defining equations;
1.522 - if needed these are implemented by program abort instead.
1.523 + \item @{command (HOL) "code_abort"} declares constants which are not
1.524 + required to have a definition by means of defining equations; if
1.525 + needed these are implemented by program abort instead.
1.526
1.527 - \item [@{attribute (HOL) code}] explicitly selects (or
1.528 - with option ``@{text "del"}'' deselects) a defining equation for
1.529 - code generation. Usually packages introducing defining equations
1.530 - provide a reasonable default setup for selection.
1.531 + \item @{attribute (HOL) code} explicitly selects (or with option
1.532 + ``@{text "del"}'' deselects) a defining equation for code
1.533 + generation. Usually packages introducing defining equations provide
1.534 + a reasonable default setup for selection.
1.535
1.536 - \item [@{attribute (HOL) code}@{text inline}] declares (or with
1.537 + \item @{attribute (HOL) code}~@{text inline} declares (or with
1.538 option ``@{text "del"}'' removes) inlining theorems which are
1.539 applied as rewrite rules to any defining equation during
1.540 preprocessing.
1.541
1.542 - \item [@{command (HOL) "print_codesetup"}] gives an overview on
1.543 + \item @{command (HOL) "print_codesetup"} gives an overview on
1.544 selected defining equations, code generator datatypes and
1.545 preprocessor setup.
1.546
1.547 - \end{descr}
1.548 + \end{description}
1.549 *}
1.550
1.551
1.552 @@ -1193,27 +1189,27 @@
1.553 decl: ((name ':')? term '(' 'overloaded' ')'?)
1.554 \end{rail}
1.555
1.556 - \begin{descr}
1.557 + \begin{description}
1.558
1.559 - \item [@{command (HOL) "specification"}~@{text "decls \<phi>"}] sets up a
1.560 + \item @{command (HOL) "specification"}~@{text "decls \<phi>"} sets up a
1.561 goal stating the existence of terms with the properties specified to
1.562 hold for the constants given in @{text decls}. After finishing the
1.563 proof, the theory will be augmented with definitions for the given
1.564 constants, as well as with theorems stating the properties for these
1.565 constants.
1.566
1.567 - \item [@{command (HOL) "ax_specification"}~@{text "decls \<phi>"}] sets
1.568 - up a goal stating the existence of terms with the properties
1.569 - specified to hold for the constants given in @{text decls}. After
1.570 - finishing the proof, the theory will be augmented with axioms
1.571 - expressing the properties given in the first place.
1.572 + \item @{command (HOL) "ax_specification"}~@{text "decls \<phi>"} sets up
1.573 + a goal stating the existence of terms with the properties specified
1.574 + to hold for the constants given in @{text decls}. After finishing
1.575 + the proof, the theory will be augmented with axioms expressing the
1.576 + properties given in the first place.
1.577
1.578 - \item [@{text decl}] declares a constant to be defined by the
1.579 + \item @{text decl} declares a constant to be defined by the
1.580 specification given. The definition for the constant @{text c} is
1.581 bound to the name @{text c_def} unless a theorem name is given in
1.582 the declaration. Overloaded constants should be declared as such.
1.583
1.584 - \end{descr}
1.585 + \end{description}
1.586
1.587 Whether to use @{command (HOL) "specification"} or @{command (HOL)
1.588 "ax_specification"} is to some extent a matter of style. @{command