--- a/ProgTutorial/FirstSteps.thy Sun Oct 11 22:45:29 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy Sun Oct 11 23:16:34 2009 +0200
@@ -352,21 +352,24 @@
comprehension of the code, but after getting familiar with them, they
actually ease the understanding and also the programming.
- The simplest combinator is @{ML_ind I}, which is just the identity function defined as
+ The simplest combinator is @{ML_ind I in Basic_Library}, which is just the
+ identity function defined as
*}
ML{*fun I x = x*}
-text {* Another simple combinator is @{ML_ind K}, defined as *}
+text {*
+ Another simple combinator is @{ML_ind K in Library}, defined as
+*}
ML{*fun K x = fn _ => x*}
text {*
- @{ML_ind K} ``wraps'' a function around the argument @{text "x"}. However, this
+ @{ML K} ``wraps'' a function around the argument @{text "x"}. However, this
function ignores its argument. As a result, @{ML K} defines a constant function
always returning @{text x}.
- The next combinator is reverse application, @{ML_ind "|>"}, defined as:
+ The next combinator is reverse application, @{ML_ind "|>" in Basics}, defined as:
*}
ML{*fun x |> f = f x*}
@@ -443,19 +446,20 @@
end"
"P z za zb"}
- You can read off this behaviour from how @{ML apply_fresh_args} is
- coded: in Line 2, the function @{ML_ind fastype_of} calculates the type of the
- term; @{ML_ind binder_types} in the next line produces the list of argument
- types (in the case above the list @{text "[nat, int, unit]"}); Line 4
- pairs up each type with the string @{text "z"}; the
- function @{ML_ind variant_frees in Variable} generates for each @{text "z"} a
- unique name avoiding the given @{text f}; the list of name-type pairs is turned
- into a list of variable terms in Line 6, which in the last line is applied
- by the function @{ML_ind list_comb} to the term. In this last step we have to
- use the function @{ML_ind curry}, because @{ML_ind list_comb} expects the
- function and the variables list as a pair. This kind of functions is often needed when
- constructing terms with fresh variables. The infrastructure helps tremendously
- to avoid any name clashes. Consider for example:
+ You can read off this behaviour from how @{ML apply_fresh_args} is coded: in
+ Line 2, the function @{ML_ind fastype_of in Term} calculates the type of the
+ term; @{ML_ind binder_types in Term} in the next line produces the list of
+ argument types (in the case above the list @{text "[nat, int, unit]"}); Line
+ 4 pairs up each type with the string @{text "z"}; the function @{ML_ind
+ variant_frees in Variable} generates for each @{text "z"} a unique name
+ avoiding the given @{text f}; the list of name-type pairs is turned into a
+ list of variable terms in Line 6, which in the last line is applied by the
+ function @{ML_ind list_comb in Term} to the term. In this last step we have
+ to use the function @{ML_ind curry in Library}, because @{ML list_comb}
+ expects the function and the variables list as a pair. This kind of
+ functions is often needed when constructing terms with fresh variables. The
+ infrastructure helps tremendously to avoid any name clashes. Consider for
+ example:
@{ML_response_fake [display,gray]
"let
@@ -470,8 +474,8 @@
where the @{text "za"} is correctly avoided.
- The combinator @{ML_ind "#>"} is the reverse function composition. It can be
- used to define the following function
+ The combinator @{ML_ind "#>" in Basics} is the reverse function composition.
+ It can be used to define the following function
*}
ML{*val inc_by_six =
@@ -485,10 +489,9 @@
composition allows you to read the code top-down.
The remaining combinators described in this section add convenience for the
- ``waterfall method'' of writing functions. The combinator @{ML_ind tap} allows
- you to get hold of an intermediate result (to do some side-calculations for
- instance). The function
-
+ ``waterfall method'' of writing functions. The combinator @{ML_ind tap in
+ Basics} allows you to get hold of an intermediate result (to do some
+ side-calculations for instance). The function
*}
ML %linenosgray{*fun inc_by_three x =
@@ -498,15 +501,15 @@
text {*
increments the argument first by @{text "1"} and then by @{text "2"}. In the
- middle (Line 3), however, it uses @{ML_ind tap} for printing the ``plus-one''
- intermediate result inside the tracing buffer. The function @{ML_ind tap} can
+ middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one''
+ intermediate result inside the tracing buffer. The function @{ML tap} can
only be used for side-calculations, because any value that is computed
cannot be merged back into the ``main waterfall''. To do this, you can use
the next combinator.
- The combinator @{ML_ind "`"} (a backtick) is similar to @{ML tap}, but applies a
- function to the value and returns the result together with the value (as a
- pair). For example the function
+ The combinator @{ML_ind "`" in Basics} (a backtick) is similar to @{ML tap},
+ but applies a function to the value and returns the result together with the
+ value (as a pair). For example the function
*}
ML{*fun inc_as_pair x =
@@ -519,8 +522,8 @@
for x}. After that, the function increments the right-hand component of the
pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}.
- The combinators @{ML_ind "|>>"} and @{ML_ind "||>"} are defined for
- functions manipulating pairs. The first applies the function to
+ The combinators @{ML_ind "|>>" in Basics} and @{ML_ind "||>" in Basics} are
+ defined for functions manipulating pairs. The first applies the function to
the first component of the pair, defined as
*}
@@ -566,8 +569,8 @@
conciseness is only small, in more complicated situations the benefit of
avoiding @{text "lets"} can be substantial.
- With the combinator @{ML_ind "|->"} you can re-combine the elements from a pair.
- This combinator is defined as
+ With the combinator @{ML_ind "|->" in Basics} you can re-combine the
+ elements from a pair. This combinator is defined as
*}
ML{*fun (x, y) |-> f = f x y*}
@@ -582,11 +585,12 @@
|-> (fn x => fn y => x + y)*}
text {*
- The combinator @{ML_ind ||>>} plays a central rôle whenever your task is to update a
- theory and the update also produces a side-result (for example a theorem). Functions
- for such tasks return a pair whose second component is the theory and the fist
- component is the side-result. Using @{ML_ind ||>>}, you can do conveniently the update
- and also accumulate the side-results. Consider the following simple function.
+ The combinator @{ML_ind ||>> in Basics} plays a central rôle whenever your
+ task is to update a theory and the update also produces a side-result (for
+ example a theorem). Functions for such tasks return a pair whose second
+ component is the theory and the fist component is the side-result. Using
+ @{ML ||>>}, you can do conveniently the update and also
+ accumulate the side-results. Consider the following simple function.
*}
ML %linenosgray{*fun acc_incs x =
@@ -597,7 +601,7 @@
text {*
The purpose of Line 2 is to just pair up the argument with a dummy value (since
- @{ML_ind "||>>"} operates on pairs). Each of the next three lines just increment
+ @{ML ||>>} operates on pairs). Each of the next three lines just increment
the value by one, but also nest the intermediate results to the left. For example
@{ML_response [display,gray]
@@ -614,14 +618,13 @@
*}
text {*
- Recall that @{ML_ind "|>"} is the reverse function application. Recall also that
- the related
- reverse function composition is @{ML_ind "#>"}. In fact all the combinators
- @{ML_ind "|->"}, @{ML_ind "|>>"} , @{ML_ind "||>"} and @{ML_ind
- "||>>"} described above have related combinators for
- function composition, namely @{ML_ind "#->"}, @{ML_ind "#>>"},
- @{ML_ind "##>"} and @{ML_ind "##>>"}.
- Using @{ML_ind "#->"}, for example, the function @{text double} can also be written as:
+ Recall that @{ML "|>"} is the reverse function application. Recall also that
+ the related reverse function composition is @{ML "#>"}. In fact all the
+ combinators @{ML "|->"}, @{ML "|>>"} , @{ML "||>"} and @{ML "||>>"}
+ described above have related combinators for function composition, namely
+ @{ML_ind "#->" in Basics}, @{ML_ind "#>>" in Basics}, @{ML_ind "##>" in
+ Basics} and @{ML_ind "##>>" in Basics}. Using @{ML "#->"}, for example, the
+ function @{text double} can also be written as:
*}
ML{*val double =
@@ -637,7 +640,7 @@
list_comb} that works over pairs to fit with the combinator @{ML "|>"}. Such
plumbing is also needed in situations where a function operate over lists,
but one calculates only with a single element. An example is the function
- @{ML_ind check_terms in Syntax}, whose purpose is to type-check a list
+ @{ML_ind check_terms in Syntax}, whose purpose is to type-check a list
of terms. Consider the code:
@{ML_response_fake [display, gray]
@@ -708,7 +711,7 @@
where @{text "@{theory}"} is an antiquotation that is substituted with the
current theory (remember that we assumed we are inside the theory
@{text FirstSteps}). The name of this theory can be extracted using
- the function @{ML_ind theory_name in Context}.
+ the function @{ML_ind theory_name in Context}.
Note, however, that antiquotations are statically linked, that is their value is
determined at ``compile-time'', not at ``run-time''. For example the function
@@ -779,7 +782,7 @@
"name"}
An example where a qualified name is needed is the function
- @{ML_ind define in LocalTheory}. This function is used below to define
+ @{ML_ind define in LocalTheory}. This function is used below to define
the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}.
*}
@@ -814,7 +817,7 @@
restriction of this antiquotation is that it does not allow you to use
schematic variables. If you want to have an antiquotation that does not have
this restriction, you can implement your own using the function @{ML_ind
- ML_Antiquote.inline}. The code for the antiquotation @{text "term_pat"} is
+ inline in ML_Antiquote}. The code for the antiquotation @{text "term_pat"} is
as follows.
*}
--- a/ProgTutorial/Parsing.thy Sun Oct 11 22:45:29 2009 +0200
+++ b/ProgTutorial/Parsing.thy Sun Oct 11 23:16:34 2009 +0200
@@ -37,7 +37,7 @@
text {*
Let us first have a look at parsing strings using generic parsing
- combinators. The function @{ML_ind "$$"} takes a string as argument and will
+ combinators. The function @{ML_ind "$$" in Scan} takes a string as argument and will
``consume'' this string from a given input list of strings. ``Consume'' in
this context means that it will return a pair consisting of this string and
the rest of the input list. For example:
@@ -71,11 +71,12 @@
However, note that these exceptions are private to the parser and cannot be accessed
by the programmer (for example to handle them).
- In the examples above we use the function @{ML_ind Symbol.explode}, instead of the
- more standard library function @{ML_ind explode}, for obtaining an input list for
- the parser. The reason is that @{ML_ind Symbol.explode} is aware of character sequences,
- for example @{text "\<foo>"}, that have a special meaning in Isabelle. To see
- the difference consider
+ In the examples above we use the function @{ML_ind explode in Symbol} in the
+ structure @{ML_struct Symbol}, instead of the more standard library function
+ @{ML_ind explode}, for obtaining an input list for the parser. The reason is
+ that @{ML_ind explode} in @{ML_struct Symbol} is aware of character
+ sequences, for example @{text "\<foo>"}, that have a special meaning in
+ Isabelle. To see the difference consider
@{ML_response_fake [display,gray]
"let
@@ -87,7 +88,7 @@
[\"\<foo>\", \" \", \"b\", \"a\", \"r\"])"}
Slightly more general than the parser @{ML "$$"} is the function
- @{ML_ind one in Scan}, in that it takes a predicate as argument and
+ @{ML_ind one in Scan}, in that it takes a predicate as argument and
then parses exactly
one item from the input list satisfying this predicate. For example the
following parser either consumes an @{text [quotes] "h"} or a @{text
@@ -103,7 +104,7 @@
end"
"((\"h\", [\"e\", \"l\", \"l\", \"o\"]),(\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
- Two parsers can be connected in sequence by using the function @{ML_ind "--"}.
+ Two parsers can be connected in sequence by using the function @{ML_ind "--" in Scan}.
For example parsing @{text "h"}, @{text "e"} and @{text "l"} (in this
order) you can achieve by:
@@ -121,7 +122,7 @@
"(\"hell\", [\"o\"])"}
Parsers that explore alternatives can be constructed using the function
- @{ML_ind "||"}. The parser @{ML "(p || q)" for p q} returns the
+ @{ML_ind "||" in Scan}. The parser @{ML "(p || q)" for p q} returns the
result of @{text "p"}, in case it succeeds, otherwise it returns the
result of @{text "q"}. For example:
@@ -136,7 +137,7 @@
end"
"((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
- The functions @{ML_ind "|--"} and @{ML_ind "--|"} work like the sequencing
+ The functions @{ML_ind "|--" in Scan} and @{ML_ind "--|" in Scan} work like the sequencing
function for parsers, except that they discard the item being parsed by the
first (respectively second) parser. For example:
@@ -164,7 +165,7 @@
end"
"((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"x\", [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
- The function @{ML_ind option in Scan} works similarly, except no default value can
+ The function @{ML_ind option in Scan} works similarly, except no default value can
be given. Instead, the result is wrapped as an @{text "option"}-type. For example:
@{ML_response [display,gray]
@@ -176,14 +177,14 @@
(p input1, p input2)
end" "((SOME \"h\", [\"e\", \"l\", \"l\", \"o\"]), (NONE, [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
- The function @{ML_ind ahead in Scan} parses some input, but leaves the original
+ The function @{ML_ind ahead in Scan} parses some input, but leaves the original
input unchanged. For example:
@{ML_response [display,gray]
"Scan.ahead (Scan.this_string \"foo\") (Symbol.explode \"foo\")"
"(\"foo\", [\"f\", \"o\", \"o\"])"}
- The function @{ML_ind "!!"} helps with producing appropriate error messages
+ The function @{ML_ind "!!" in Scan} helps with producing appropriate error messages
during parsing. For example if you want to parse @{text p} immediately
followed by @{text q}, or start a completely different parser @{text r},
you might write:
@@ -219,13 +220,13 @@
then the parsing aborts and the error message @{text "foo"} is printed. In order to
see the error message properly, you need to prefix the parser with the function
- @{ML_ind error in Scan}. For example:
+ @{ML_ind error in Scan}. For example:
@{ML_response_fake [display,gray]
"Scan.error (!! (fn _ => \"foo\") ($$ \"h\"))"
"Exception Error \"foo\" raised"}
- This ``prefixing'' is usually done by wrappers such as @{ML_ind local_theory in OuterSyntax}
+ This ``prefixing'' is usually done by wrappers such as @{ML_ind local_theory in OuterSyntax}
(see Section~\ref{sec:newcommand} which explains this function in more detail).
Let us now return to our example of parsing @{ML "(p -- q) || r" for p q
@@ -262,14 +263,14 @@
@{ML_response [display,gray] "Scan.repeat ($$ \"h\") (Symbol.explode \"hhhhello\")"
"([\"h\", \"h\", \"h\", \"h\"], [\"e\", \"l\", \"l\", \"o\"])"}
- Note that @{ML_ind repeat in Scan} stores the parsed items in a list. The function
- @{ML_ind repeat1 in Scan} is similar, but requires that the parser @{text "p"}
+ Note that @{ML_ind repeat in Scan} stores the parsed items in a list. The function
+ @{ML_ind repeat1 in Scan} is similar, but requires that the parser @{text "p"}
succeeds at least once.
Also note that the parser would have aborted with the exception @{text MORE}, if
you had it run with the string @{text [quotes] "hhhh"}. This can be avoided by using
- the wrapper @{ML_ind finite in Scan} and the ``stopper-token''
- @{ML_ind stopper in Symbol}. With them you can write:
+ the wrapper @{ML_ind finite in Scan} and the ``stopper-token''
+ @{ML_ind stopper in Symbol}. With them you can write:
@{ML_response [display,gray] "Scan.finite Symbol.stopper (Scan.repeat ($$ \"h\")) (Symbol.explode \"hhhh\")"
"([\"h\", \"h\", \"h\", \"h\"], [])"}
@@ -278,7 +279,7 @@
other stoppers need to be used when parsing, for example, tokens. However, this kind of
manually wrapping is often already done by the surrounding infrastructure.
- The function @{ML_ind repeat in Scan} can be used with @{ML_ind one in Scan} to read any
+ The function @{ML_ind repeat in Scan} can be used with @{ML_ind one in Scan} to read any
string as in
@{ML_response [display,gray]
@@ -290,10 +291,10 @@
end"
"([\"f\", \"o\", \"o\", \" \", \"b\", \"a\", \"r\", \" \", \"f\", \"o\", \"o\"], [])"}
- where the function @{ML_ind not_eof in Symbol} ensures that we do not read beyond the
+ where the function @{ML_ind not_eof in Symbol} ensures that we do not read beyond the
end of the input string (i.e.~stopper symbol).
- The function @{ML_ind unless in Scan} takes two parsers: if the first one can
+ The function @{ML_ind unless in Scan} takes two parsers: if the first one can
parse the input, then the whole parser fails; if not, then the second is tried. Therefore
@{ML_response_fake_both [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (Symbol.explode \"hello\")"
@@ -306,7 +307,7 @@
succeeds.
- The functions @{ML_ind repeat in Scan} and @{ML_ind unless in Scan} can
+ The functions @{ML_ind repeat in Scan} and @{ML_ind unless in Scan} can
be combined to read any input until a certain marker symbol is reached. In the
example below the marker symbol is a @{text [quotes] "*"}.
@@ -324,7 +325,7 @@
After parsing is done, you almost always want to apply a function to the parsed
- items. One way to do this is the function @{ML_ind ">>"} where
+ items. One way to do this is the function @{ML_ind ">>" in Scan} where
@{ML "(p >> f)" for p f} runs
first the parser @{text p} and upon successful completion applies the
function @{text f} to the result. For example
@@ -352,7 +353,7 @@
where the single-character strings in the parsed output are transformed
back into one string.
- The function @{ML_ind lift in Scan} takes a parser and a pair as arguments. This function applies
+ The function @{ML_ind lift in Scan} takes a parser and a pair as arguments. This function applies
the given parser to the second component of the pair and leaves the first component
untouched. For example
@@ -393,11 +394,11 @@
\end{readmore}
The structure @{ML_struct OuterLex} defines several kinds of tokens (for
- example @{ML_ind Ident in OuterLex} for identifiers, @{ML Keyword in
- OuterLex} for keywords and @{ML_ind Command in OuterLex} for commands). Some
+ example @{ML_ind Ident in OuterLex} for identifiers, @{ML Keyword in
+ OuterLex} for keywords and @{ML_ind Command in OuterLex} for commands). Some
token parsers take into account the kind of tokens. The first example shows
how to generate a token list out of a string using the function
- @{ML_ind scan in OuterSyntax}. It is given the argument
+ @{ML_ind scan in OuterSyntax}. It is given the argument
@{ML "Position.none"} since,
at the moment, we are not interested in generating precise error
messages. The following code\footnote{Note that because of a possible bug in
@@ -415,7 +416,7 @@
other syntactic category. The second indicates a space.
We can easily change what is recognised as a keyword with the function
- @{ML_ind keyword in OuterKeyword}. For example calling it with
+ @{ML_ind keyword in OuterKeyword}. For example calling it with
*}
ML{*val _ = OuterKeyword.keyword "hello"*}
@@ -430,7 +431,7 @@
Many parsing functions later on will require white space, comments and the like
to have already been filtered out. So from now on we are going to use the
- functions @{ML filter} and @{ML_ind is_proper in OuterLex} to do this.
+ functions @{ML filter} and @{ML_ind is_proper in OuterLex} to do this.
For example:
@{ML_response_fake [display,gray]
@@ -468,10 +469,10 @@
end"
"([\"}\", \"{\", \<dots>], [\"\<rightleftharpoons>\", \"\<leftharpoondown>\", \<dots>])"}
- You might have to adjust the @{ML_ind print_depth} in order to
+ You might have to adjust the @{ML_ind print_depth} in order to
see the complete list.
- The parser @{ML_ind "$$$" in OuterParse} parses a single keyword. For example:
+ The parser @{ML_ind "$$$" in OuterParse} parses a single keyword. For example:
@{ML_response [display,gray]
"let
@@ -482,7 +483,7 @@
end"
"((\"where\",\<dots>), (\"|\",\<dots>))"}
- Any non-keyword string can be parsed with the function @{ML_ind reserved in OuterParse}.
+ Any non-keyword string can be parsed with the function @{ML_ind reserved in OuterParse}.
For example:
@{ML_response [display,gray]
@@ -494,7 +495,7 @@
end"
"(\"bar\",[])"}
- Like before, you can sequentially connect parsers with @{ML_ind "--"}. For example:
+ Like before, you can sequentially connect parsers with @{ML "--"}. For example:
@{ML_response [display,gray]
"let
@@ -558,7 +559,7 @@
\begin{exercise} (FIXME)
A type-identifier, for example @{typ "'a"}, is a token of
- kind @{ML_ind Keyword in OuterLex}. It can be parsed using
+ kind @{ML_ind Keyword in OuterLex}. It can be parsed using
the function @{ML type_ident in OuterParse}.
\end{exercise}
@@ -739,7 +740,7 @@
variables with optional type-annotation and syntax-annotation, and a list of
rules where every rule has optionally a name and an attribute.
- The function @{ML_ind "fixes" in OuterParse} in Line 2 of the parser reads an
+ The function @{ML_ind "fixes" in OuterParse} in Line 2 of the parser reads an
\isacommand{and}-separated
list of variables that can include optional type annotations and syntax translations.
For example:\footnote{Note that in the code we need to write
@@ -763,8 +764,8 @@
not yet used to type the variables: this must be done by type-inference later
on. Since types are part of the inner syntax they are strings with some
encoded information (see previous section). If a mixfix-syntax is
- present for a variable, then it is stored in the @{ML_ind Mixfix} data structure;
- no syntax translation is indicated by @{ML_ind NoSyn}.
+ present for a variable, then it is stored in the @{ML_ind Mixfix} data structure;
+ no syntax translation is indicated by @{ML_ind NoSyn}.
\begin{readmore}
The data structure for mixfix annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}.
@@ -773,7 +774,7 @@
Lines 3 to 7 in the function @{ML spec_parser} implement the parser for a
list of introduction rules, that is propositions with theorem annotations
such as rule names and attributes. The introduction rules are propositions
- parsed by @{ML_ind prop in OuterParse}. However, they can include an optional
+ parsed by @{ML_ind prop in OuterParse}. However, they can include an optional
theorem name plus some attributes. For example
@{ML_response [display,gray] "let
@@ -783,8 +784,8 @@
(name, map Args.dest_src attrib)
end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"}
- The function @{ML_ind opt_thm_name in SpecParse} is the ``optional'' variant of
- @{ML_ind thm_name in SpecParse}. Theorem names can contain attributes. The name
+ The function @{ML_ind opt_thm_name in SpecParse} is the ``optional'' variant of
+ @{ML_ind thm_name in SpecParse}. Theorem names can contain attributes. The name
has to end with @{text [quotes] ":"}---see the argument of
the function @{ML SpecParse.opt_thm_name} in Line 7.
@@ -799,7 +800,7 @@
Have a look at how the parser @{ML SpecParse.where_alt_specs} is implemented
in file @{ML_file "Pure/Isar/spec_parse.ML"}. This parser corresponds
to the ``where-part'' of the introduction rules given above. Below
- we paraphrase the code of @{ML_ind where_alt_specs in SpecParse} adapted to our
+ we paraphrase the code of @{ML_ind where_alt_specs in SpecParse} adapted to our
purposes.
\begin{isabelle}
*}
@@ -850,7 +851,7 @@
end *}
text {*
- The crucial function @{ML_ind local_theory in OuterSyntax} expects a name for the command, a
+ The crucial function @{ML_ind local_theory in OuterSyntax} expects a name for the command, a
short description, a kind indicator (which we will explain later more thoroughly) and a
parser producing a local theory transition (its purpose will also explained
later).
@@ -996,7 +997,7 @@
The crucial part of a command is the function that determines the behaviour
of the command. In the code above we used a ``do-nothing''-function, which
- because of @{ML_ind succeed in Scan} does not parse any argument, but immediately
+ because of @{ML_ind succeed in Scan} does not parse any argument, but immediately
returns the simple function @{ML "LocalTheory.theory I"}. We can
replace this code by a function that first parses a proposition (using the
parser @{ML OuterParse.prop}), then prints out the tracing
@@ -1022,7 +1023,7 @@
foobar_trace "True \<and> False"
text {*
- Note that so far we used @{ML_ind thy_decl in OuterKeyword} as the kind
+ Note that so far we used @{ML_ind thy_decl in OuterKeyword} as the kind
indicator for the command. This means that the command finishes as soon as
the arguments are processed. Examples of this kind of commands are
\isacommand{definition} and \isacommand{declare}. In other cases, commands
@@ -1030,7 +1031,7 @@
``open up'' a proof in order to prove the proposition (for example
\isacommand{lemma}) or prove some other properties (for example
\isacommand{function}). To achieve this kind of behaviour, you have to use
- the kind indicator @{ML_ind thy_goal in OuterKeyword} and the function @{ML
+ the kind indicator @{ML_ind thy_goal in OuterKeyword} and the function @{ML
"local_theory_to_proof" in OuterSyntax} to set up the command. Note,
however, once you change the ``kind'' of a command from @{ML thy_decl in
OuterKeyword} to @{ML thy_goal in OuterKeyword} then the keyword file needs
@@ -1059,8 +1060,8 @@
text {*
The function @{text goal_prop} in Lines 2 to 7 takes a string (the proposition to be
proved) and a context as argument. The context is necessary in order to be able to use
- @{ML_ind read_prop in Syntax}, which converts a string into a proper proposition.
- In Line 6 the function @{ML_ind theorem_i in Proof} starts the proof for the
+ @{ML_ind read_prop in Syntax}, which converts a string into a proper proposition.
+ In Line 6 the function @{ML_ind theorem_i in Proof} starts the proof for the
proposition. Its argument @{ML NONE} stands for a locale (which we chose to
omit); the argument @{ML "(K I)"} stands for a function that determines what
should be done with the theorem once it is proved (we chose to just forget
@@ -1085,7 +1086,7 @@
text {*
{\bf TBD below}
- (FIXME: read a name and show how to store theorems; see @{ML_ind note in LocalTheory})
+ (FIXME: read a name and show how to store theorems; see @{ML_ind note in LocalTheory})
*}
@@ -1266,7 +1267,7 @@
It defines the method @{text foo}, which takes no arguments (therefore the
parser @{ML Scan.succeed}) and only applies a single tactic, namely the tactic which
applies @{thm [source] conjE} and then @{thm [source] conjI}. The function
- @{ML_ind SIMPLE_METHOD}
+ @{ML_ind SIMPLE_METHOD in Method}
turns such a tactic into a method. The method @{text "foo"} can be used as follows
*}