isabelle-cookbook: comparison ProgTutorial/Parsing.thy

equal deleted inserted replaced

-:615762b8d8cb
+:9728b0432fb2
 whereby @{ML_ind "thy_decl" in Keyword} indicates the kind of the
 command.  Another possible kind is @{text "thy_goal"}, or you can
 also to omit the kind entirely, in which case you declare a keyword
 (something that is part of a command).
-Now you can implement \isacommand{foobar} as:
+Now you can implement \isacommand{foobar} as follows.
 *}
 ML %grayML{*let
 val do_nothing = Scan.succeed (Local_Theory.background_theory I)
 in
 a parser producing a local theory transition (explained later). For the
 name and the kind, you can use the ML-antiquotation @{text "@{command_spec ...}"}.
 After this, you can write in your theory
 *}
 foobar
+text {*
-text {*
+but of course you will not see ``anything''.
-Remember that this only works in jEdit. In order to let Proof-General
+Remember that this only works in jEdit. In order to enable also Proof-General
 recognise this command, a keyword file needs to be generated (see next
 section).
 At the moment the command \isacommand{foobar} is not very useful. Let us
 refine it a bit next by letting it take a proposition as argument and
 printing this proposition inside the tracing buffer. We announce the
-command as
+command in the theory header as
 \begin{graybox}
 \isacommand{keywords} @{text [quotes] "foobar_trace"} @{text "::"} @{text "thy_decl"}
 \end{graybox}
 "traces a proposition"
 (Parse.prop >> trace_prop)
 end *}
 text {*
-The command is now \isacommand{foobar\_trace} and can be used to
+This command can now be used to
 see the proposition in the tracing buffer.
 *}
 foobar_trace "True \<and> False"
 the kind indicator @{ML_ind thy_goal in Keyword} and the function @{ML
 "local_theory_to_proof" in Outer_Syntax} to set up the command.
 Below we show the command \isacommand{foobar\_goal} which takes a
 proposition as argument and then starts a proof in order to prove
 it. Therefore, we need to announce this command in the header
-as @{text "thy_goal"}
+as @{text "thy_goal"}.
 \begin{graybox}
 \isacommand{keywords} @{text [quotes] "foobar_goal"} @{text "::"} @{text "thy_goal"}
 \end{graybox}
 apply(rule conjI)
 apply(rule TrueI)+
 done
 text {*
-The final new command we describe is
+The last command we describe here is
 \isacommand{foobar\_proof}. Like \isacommand{lemma}, its purpose is
 to take a proposition and open a corresponding proof-state that
 allows us to give a proof for it. However, unlike
-\isacommand{lemma}, the proposition will be given as an
+\isacommand{lemma}, the proposition will be given as a
 ML-value. Such a command is quite useful during development
-of a tool that generates a goal on the ML-level and you want to see
+when you generate a goal on the ML-level and want to see
-whether it is provable. In addition you also want that the proved
+whether it is provable. In addition allow the proved
-proposition can be given a lemma name that can be referenced later on.
+proposition to have a name that can be referenced later on.
-The first problem of this new command is to parse some text as
+The first problem for this command is to parse some text as
-ML-source and then interpret it as a term. For the parsing we can
+ML-source and then interpret it as an Isabelle term. For the parsing we can
 use the function @{ML_ind "ML_source" in Parse} in the structure
 @{ML_struct Parse}. For running the ML-interpreter we need the
 following scaffolding code.
 *}
 fun init thy () = error "Result")
 val result_cookie = (Result.get, Result.put, "Result.put") *}
 text {*
-With this in place we can write the code for \isacommand{foobar\_prove}.
+With this in place, we can write the code for \isacommand{foobar\_prove}.
 *}
 ML %linenosgray{*let
 fun after_qed thm_name thms lthy =
 Local_Theory.note (thm_name, (flat thms)) lthy |> snd
 (parser >> setup_proof)
 end*}
 text {*
 In Line 12, we implement a parser that first reads in an optional lemma name (terminated
-by ``:'') and then some ML-code. The function in Lines 5 to 10 takes the ML
+by ``:'') and then some ML-code. The function in Lines 5 to 10 takes the ML-text
-text and lets the ML-runtime evaluate it using the function @{ML_ind value in Code_Runtime}
+and lets the ML-runtime evaluate it using the function @{ML_ind value in Code_Runtime}
 in the structure @{ML_struct Code_Runtime}.  Once the ML-text has been turned into a term,
 the function @{ML theorem in Proof} opens a corresponding proof-state. This function takes the
 function @{ML_text "after_qed"} as argument, whose purpose is to store the theorem,
-once it is proven, under the user given name @{text "thm_name"}.
+once it is proven, under the given name @{text "thm_name"}.
-We can now give take a term, for example
+You can now define a term, for example
 *}
 ML %grayML{*val prop_true = @{prop "True"}*}
 text {*
-and give a proove for it using \isacommand{foobar\_prove}:
+and give it a proof using \isacommand{foobar\_prove}:
 *}
 foobar_prove test: prop_true
 apply(rule TrueI)
 done

changeset 521	9728b0432fb2
parent 520	615762b8d8cb
child 522	0ed6f49277c4