--- a/ProgTutorial/Advanced.thy Thu Nov 17 12:20:19 2011 +0000
+++ b/ProgTutorial/Advanced.thy Thu Nov 17 16:33:49 2011 +0000
@@ -165,7 +165,8 @@
val (_, tmp_thy') = Sign.declare_const @{context} foo_const tmp_thy
val trm1 = Syntax.read_term_global tmp_thy' "FOO baz"
val trm2 = Syntax.read_term_global thy "FOO baz"
- val _ = writeln (@{make_string} trm1 ^ "\n" ^ @{make_string} trm2)
+ val _ = pwriteln
+ (Pretty.str (@{make_string} trm1 ^ "\n" ^ @{make_string} trm2))
in
thy
end *}
@@ -192,6 +193,11 @@
inference. This is relevant in situations where definitions are made later,
but parsing and type inference has to take already proceed as if the definitions
were already made.
+
+ \begin{readmore}
+ Most of the functions about theories are implemented in
+ @{ML_file "Pure/theory.ML"} and @{ML_file "Pure/global_theory.ML"}.
+ \end{readmore}
*}
section {* Contexts *}
@@ -315,7 +321,7 @@
"([\"y\", \"ya\", \"z\"], ...)"}
Now a fresh variant for the second occurence of @{text y} is created
- avoiding any clash. In this way we can also create free variables
+ avoiding any clash. In this way we can also create fresh free variables
that avoid any clashes with fixed variables. In Line~3 below we fix
the variable @{text x} in the context @{text ctxt1}. Next we want to
create two fresh variables of type @{typ nat} as variants of the
@@ -459,10 +465,11 @@
end"
"?P ?x ?y ?z ?x ?y ?z"}
- Since we fixed all variables in @{text ctxt1}, in the result all of them
- are schematic. The great point of contexts is that exporting from one to
- another is not just concerned with variables, but also assumptions. For this we
- can use the function @{ML_ind export in Assumption} from the structure
+ Since we fixed all variables in @{text ctxt1}, in the exported
+ result all of them are schematic. The great point of contexts is
+ that exporting from one to another is not just restricted to
+ variables, but also works with assumptions. For this we can use the
+ function @{ML_ind export in Assumption} from the structure
@{ML_struct Assumption}. Consider the following code.
@{ML_response_fake [display, gray, linenos]
@@ -552,7 +559,7 @@
oops
*)
-section {* Local Theories (TBD) *}
+section {* Local Theories and Local Setups\label{sec:local} (TBD) *}
text {*
In contrast to an ordinary theory, which simply consists of a type
--- a/ProgTutorial/Essential.thy Thu Nov 17 12:20:19 2011 +0000
+++ b/ProgTutorial/Essential.thy Thu Nov 17 16:33:49 2011 +0000
@@ -115,12 +115,13 @@
end"
"?x3, ?x1.3, x"}
- When constructing terms, you are usually concerned with free variables (as
- mentioned earlier, you cannot construct schematic variables using the
- antiquotation @{text "@{term \<dots>}"}). If you deal with theorems, you have to,
- however, observe the distinction. The reason is that only schematic
- variables can be instantiated with terms when a theorem is applied. A
- similar distinction between free and schematic variables holds for types
+ When constructing terms, you are usually concerned with free
+ variables (as mentioned earlier, you cannot construct schematic
+ variables using the built in antiquotation \mbox{@{text "@{term
+ \<dots>}"}}). If you deal with theorems, you have to, however, observe the
+ distinction. The reason is that only schematic variables can be
+ instantiated with terms when a theorem is applied. A similar
+ distinction between free and schematic variables holds for types
(see below).
\begin{readmore}
@@ -1555,8 +1556,10 @@
While we obtained a theorem as result, this theorem is not
yet stored in Isabelle's theorem database. Consequently, it cannot be
referenced on the user level. One way to store it in the theorem database is
- by using the function @{ML_ind note in Local_Theory}.\footnote{\bf FIXME: make sure a pointer
- to the section about local-setup is given here.}
+ by using the function @{ML_ind note in Local_Theory} from the structure
+ @{ML_struct Local_Theory} (the Isabelle command
+ \isacommand{local\_setup} will be explained in more detail in
+ Section~\ref{sec:local}).
*}
local_setup %gray {*
@@ -1598,7 +1601,7 @@
[source] my_thm_simp} is that they can now also be referenced with the
\isacommand{thm}-command on the user-level of Isabelle
-
+
\begin{isabelle}
\isacommand{thm}~@{text "my_thm my_thm_simp"}\isanewline
@{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}\isanewline
@@ -2009,16 +2012,20 @@
using @{text "@{thm \<dots>}"} produces
\begin{isabelle}
+ \begin{graybox}
@{text "@{thm style_test}"}\\
@{text ">"}~@{thm style_test}
+ \end{graybox}
\end{isabelle}
as expected. But with the theorem style @{text "@{thm (my_strip_allq) \<dots>}"}
we obtain
\begin{isabelle}
+ \begin{graybox}
@{text "@{thm (my_strip_allq) style_test}"}\\
@{text ">"}~@{thm (my_strip_allq) style_test}
+ \end{graybox}
\end{isabelle}
without the leading quantifiers. We can improve this theorem style by explicitly
@@ -2051,10 +2058,11 @@
on the resulting term. We can now suggest, for example, two variables for
stripping off the first two @{text \<forall>}-quantifiers.
-
\begin{isabelle}
+ \begin{graybox}
@{text "@{thm (my_strip_allq2 x' x'') style_test}"}\\
@{text ">"}~@{thm (my_strip_allq2 x' x'') style_test}
+ \end{graybox}
\end{isabelle}
Such styles allow one to print out theorems in documents formatted to
--- a/ProgTutorial/First_Steps.thy Thu Nov 17 12:20:19 2011 +0000
+++ b/ProgTutorial/First_Steps.thy Thu Nov 17 16:33:49 2011 +0000
@@ -76,8 +76,8 @@
\end{isabelle}
\end{quote}
- However, both commands will only play minor roles in this tutorial (we will
- always arrange that the ML-code is defined outside proofs).
+ However, both commands will only play minor roles in this tutorial (we most of
+ the time make sure that the ML-code is defined outside proofs).
@@ -211,11 +211,14 @@
where now even @{term Pair} is written with its type (@{term Pair} is the
term-constructor for products). Other configuration values that influence
- printing of terms include @{ML_ind show_brackets in Syntax}, @{ML_ind
- show_sorts in Syntax} and @{ML_ind eta_contract in Syntax}.
-*}
+ printing of terms include
-text {*
+ \begin{itemize}
+ \item @{ML_ind show_brackets in Syntax}
+ \item @{ML_ind show_sorts in Syntax}
+ \item @{ML_ind eta_contract in Syntax}
+ \end{itemize}
+
A @{ML_type cterm} can be printed with the following function.
*}
@@ -689,8 +692,8 @@
pwriteln (pretty_term ctxt' one_trm);
pwriteln (pretty_thm ctxt' one_thm)
end"
- "one
-one \<equiv> 1"}
+ "One
+One \<equiv> 1"}
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 "||>>"}
@@ -701,8 +704,8 @@
*}
ML{*val double =
- (fn x => (x, x))
- #-> (fn x => fn y => x + y)*}
+ (fn x => (x, x)) #->
+ (fn x => fn y => x + y)*}
text {*
--- a/ProgTutorial/Intro.thy Thu Nov 17 12:20:19 2011 +0000
+++ b/ProgTutorial/Intro.thy Thu Nov 17 16:33:49 2011 +0000
@@ -223,7 +223,7 @@
this. Still to keep them to a minimum, you can submit your changes first to a rather
sophisticated \emph{testboard}, which will perform checks of your changes against the
Isabelle repository and against the AFP. The advantage of the testboard is
- that the testing is performed by rather powerful machines, saving you lengthy
+ that the testing is performed by rather powerful machines saving you lengthy
tests on, for example, your own laptop. You can see the results of the testboard
at
@@ -241,7 +241,7 @@
where the dots need to be replaced by your login name. Note that for
pushing changes to the testboard you need to add the option @{text "-f"},
- which however should \emph{never} be used with the main Isabelle
+ which should \emph{never} be used with the main Isabelle
repository. While the testboard is a great system for supporting Isabelle
developers, its disadvantage is that it needs login permissions for the
computers in Munich. So in order to use it, you might have to ask other
Binary file progtutorial.pdf has changed