isabelle-cookbook: comparison CookBook/Package/Ind

equal deleted inserted replaced

-:bbb2d5f1d58d
+:14c3dd5ee2ad
 @{ML_struct Scan} defined in the file @{ML_file "Pure/General/scan.ML"} in the Isabelle
 sources. While these combinators do not make any assumptions about the concrete
 structure of the tokens used, the second part of the library consists of combinators
 for dealing with specific token types.
 The following is an excerpt from the signature of @{ML_struct Scan}:
-\begin{mytable}
+\begin{table}
 @{ML "|| : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b"} \\
 @{ML "-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e"} \\
 @{ML "|-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e"} \\
 @{ML "--| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e"} \\
 @{ML "optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a" in Scan} \\
 @{ML "repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a" in Scan} \\
 @{ML "repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a" in Scan} \\
 @{ML ">> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c"} \\
 @{ML "!! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b"}
-\end{mytable}
+\end{table}
 Interestingly, the functions shown above are so generic that they do not
 even rely on the input and output of the parser being a list of tokens.
 If \texttt{p} succeeds, i.e.\ does not raise an exception, the parser
 @{ML "p || q" for p q} returns the result of \texttt{p}, otherwise it returns
 the result of \texttt{q}. The parser @{ML "p -- q" for p q} first parses an
 So far, we have only looked at combinators that construct more complex parsers
 from simpler parsers. In order for these combinators to be useful, we also need
 some basic parsers. As an example, we consider the following two parsers
 defined in @{ML_struct Scan}:
-\begin{mytable}
+\begin{table}
 @{ML "one: ('a -> bool) -> 'a list -> 'a * 'a list" in Scan} \\
 @{ML "$$ : string -> string list -> string * string list"}
-\end{mytable}
+\end{table}
 The parser @{ML "one pred" for pred in Scan} parses exactly one token that
 satisfies the predicate \texttt{pred}, whereas @{ML "$$ s" for s} only
 accepts a token that equals the string \texttt{s}. Note that we can easily
 express @{ML "$$ s" for s} using @{ML "one" in Scan}:
 @{ML [display] "one (fn s' => s' = s)" for s in Scan}
 of proof methods and attributes use the token type @{ML_type OuterParse.token},
 which is identical to @{ML_type OuterLex.token}.
 The parser functions for the theory syntax are contained in the structure
 @{ML_struct OuterParse} defined in the file @{ML_file "Pure/Isar/outer_parse.ML"}.
 In our parser, we will use the following functions:
-\begin{mytable}
+\begin{table}
 @{ML "$$$ : string -> token list -> string * token list" in OuterParse} \\
 @{ML "enum1: string -> (token list -> 'a * token list) -> token list ->
 'a list * token list" in OuterParse} \\
 @{ML "prop: token list -> string * token list" in OuterParse} \\
 @{ML "opt_target: token list -> string option * token list" in OuterParse} \\
 @{ML "fixes: token list ->
 (Binding.T * string option * mixfix) list * token list" in OuterParse} \\
 @{ML "for_fixes: token list ->
 (Binding.T * string option * mixfix) list * token list" in OuterParse} \\
 @{ML "!!! : (token list -> 'a) -> token list -> 'a" in OuterParse}
-\end{mytable}
+\end{table}
 The parsers @{ML "$$$" in OuterParse} and @{ML "!!!" in OuterParse} are
 defined using the parsers @{ML "one" in Scan} and @{ML "!!"} from
 @{ML_struct Scan}.
 The parser @{ML "enum1 s p" for s p in OuterParse} parses a non-emtpy list of items
 recognized by the parser \texttt{p}, where the items are separated by \texttt{s}.
 The lists of names of the predicates and parameters, together with optional
 types and syntax, are parsed using the functions @{ML "fixes" in OuterParse}
 and @{ML for_fixes in OuterParse}, respectively.
 In addition, the following function from @{ML_struct SpecParse} for parsing
 an optional theorem name and attribute, followed by a delimiter, will be useful:
-\begin{mytable}
+\begin{table}
 @{ML "opt_thm_name:
 string -> token list -> Attrib.binding * token list" in SpecParse}
-\end{mytable}
+\end{table}
 We now have all the necessary tools to write the parser for our
 \isa{\isacommand{simple{\isacharunderscore}inductive}} command:
 @{ML_chunk [display] syntax}
 The definition of the parser \verb!ind_decl! closely follows the railroad
 diagram shown above. In order to make the code more readable, the structures

changeset 71	14c3dd5ee2ad
parent 60	5b9c6010897b
child 76	b99fa5fa63fc