--- a/CookBook/Base.thy Mon Jan 26 12:29:01 2009 +0000
+++ b/CookBook/Base.thy Mon Jan 26 12:29:43 2009 +0000
@@ -15,4 +15,5 @@
Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt))));
*}
+
end
--- a/CookBook/Intro.thy Mon Jan 26 12:29:01 2009 +0000
+++ b/CookBook/Intro.thy Mon Jan 26 12:29:43 2009 +0000
@@ -11,10 +11,8 @@
of Isabelle programming, and to explain tricks of the trade. The code
provided in the Cookbook is as far as possible checked against recent
versions of Isabelle. If something does not work, then please let us
- know. If you have comments or like to add to the Cookbook, you are very
- welcome! The Cookbook will {\bf only} remain to be helpful, if it gets constantly
- updated.
-
+ know. If you have comments or like to add to the Cookbook,
+ feel free--you are very welcome!
*}
section {* Intended Audience and Prior Knowledge *}
@@ -64,11 +62,12 @@
*}
-section {* Conventions *}
+section {* Conventions in the Cookbook *}
text {*
- All ML-code in this Cookbook is shown in highlighed displays, such as:
+ All ML-code in this Cookbook is shown in highlighed displays, like the following
+ ML-expression.
\begin{isabelle}
\begin{graybox}
@@ -82,25 +81,26 @@
This corresponds to how code can be processed inside the interactive
environment of Isabelle. However, for better readability we will drop
the enclosing \isacommand{ML} \isa{\isacharverbatimopen \ldots
- \isacharverbatimclose} and just show
+ \isacharverbatimclose} and just write
@{ML [display,gray] "3 + 4"}
- for the code above. Whenever appropriate we show the response of the code
- when evaluated. The response is prefixed with a @{text [quotes] ">"}", like
+ for the code above. Whenever appropriate we also show the response of the code
+ when evaluated. The response is prefixed with a @{text [quotes] ">"}" like
@{ML_response [display,gray] "3 + 4" "7"}
- Isabelle commands are written in bold. For example \isacommand{lemma},
- \isacommand{foobar} and so on. We use @{text "$"} to indicate a command
- needs to be run on the Unix-command line, like
+ Isabelle commands are written in bold, for example \isacommand{lemma},
+ \isacommand{foobar} and so on. We use @{text "$"} to indicate that
+ a command needs to be run on the Unix-command line, for example
@{text [display] "$ ls -la"}
- Pointers to further information and files are indicated as follows:
+ Pointers to further information and Isabelle files are highlighted
+ as follows:
\begin{readmore}
- Further information.
+ Further information or pointer to file.
\end{readmore}
*}
--- a/CookBook/Parsing.thy Mon Jan 26 12:29:01 2009 +0000
+++ b/CookBook/Parsing.thy Mon Jan 26 12:29:43 2009 +0000
@@ -580,11 +580,10 @@
recognise \isacommand{foobar} as a command. Such a keyword file can be
generated with the command-line:
-
@{text [display] "$ isabelle keywords -k foobar some_log_files"}
The option @{text "-k foobar"} indicates which postfix the name of the keyword file
- will be assigned. In the case above the generated file will be named @{text
+ will be assigned. In the case above the file will be named @{text
"isar-keywords-foobar.el"}. As can be seen, this command requires log files to be
present (in order to extract the keywords from them). To generate these log
files, we first package the code above into a separate theory file named
@@ -608,7 +607,7 @@
end"}\\
\isa{\isacharverbatimclose}\\
\isacommand{end}
- \end{graybox}\\[-4mm]
+ \end{graybox}
\caption{\small The file @{text "Command.thy"} is necessary for generating a log
file. This log file enables Isabelle to generate a keyword file containing
the command \isacommand{foobar}.\label{fig:commandtheory}}
@@ -681,15 +680,17 @@
@{text [display]
"$ isabelle keywords -k foobar
- $ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral.gz,HOL-FoobarCommand.gz}"}
+ $ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral.gz,HOL-FoobarCommand.gz}"}
- The result is the file @{text "isar-keywords-foobar.el"}. It should contain the
- string @{text "foobar"} twice (check for example that @{text "grep foobar
- isar-keywords-foobar.el"} returns something non-empty). This keyword file
- needs to be copied into the directory @{text "~/.isabelle/etc"}. To make
- Isabelle aware of this keyword file, we have to start Isabelle with the option @{text
+ The result is the file @{text "isar-keywords-foobar.el"}. It should contain
+ the string @{text "foobar"} twice (to see whether things went wrong, check
+ that @{text "grep foobar"} on this file returns something
+ non-empty). This keyword file needs to
+ be copied into the directory @{text "~/.isabelle/etc"}. To make Isabelle
+ aware of this keyword file, we have to start Isabelle with the option @{text
"-k foobar"}, i.e.
+
@{text [display] "$ isabelle -k foobar a_theory_file"}
If we now build a theory on top of @{text "Command.thy"},
@@ -779,7 +780,7 @@
proof state:
\begin{isabelle}
- \isacommand{foobar}~@{text [quotes] "True \<and> False"}\\
+ \isacommand{foobar}~@{text [quotes] "True \<and> True"}\\
@{text "goal (1 subgoal)"}\\
@{text "1. True \<and> True"}
\end{isabelle}
@@ -787,7 +788,7 @@
and we can build the proof
\begin{isabelle}
- \isacommand{foobar}~@{text [quotes] "True \<and> False"}\\
+ \isacommand{foobar}~@{text [quotes] "True \<and> True"}\\
\isacommand{apply}@{text "(rule conjI)"}\\
\isacommand{apply}@{text "(rule TrueI)+"}\\
\isacommand{done}
@@ -796,14 +797,13 @@
(FIXME What does @{text "Toplevel.theory"} @{text "Toplevel.print"}?)
- (FIXME Explain @{text "OuterKeyword.thy_decl"} and parser)
-
(FIXME read a name and show how to store theorems)
(FIXME possibly also read a locale)
*}
(*<*)
+
chapter {* Parsing *}
text {*
@@ -1472,5 +1472,4 @@
*}
(*>*)
-
end
\ No newline at end of file
--- a/CookBook/Solutions.thy Mon Jan 26 12:29:01 2009 +0000
+++ b/CookBook/Solutions.thy Mon Jan 26 12:29:43 2009 +0000
@@ -41,11 +41,14 @@
@{ML scan_all} retruns a string, instead of the pair a parser would
normally return. For example:
- @{ML_response [display,gray] "scan_all (explode \"foo bar\")" "\"foo bar\""}
-
- @{ML_response [display,gray] "scan_all (explode \"foo (*test*) bar (*test*)\")"
- "\"foo (**test**) bar (**test**)\""}
-
+ @{ML_response [display,gray]
+"let
+ val input1 = (explode \"foo bar\")
+ val input2 = (explode \"foo (*test*) bar (*test*)\")
+ in
+ (scan_all input1, scan_all input2)
+ end"
+"(\"foo bar\",\"foo (**test**) bar (**test**)\")"}
*}
end
\ No newline at end of file
Binary file cookbook.pdf has changed