--- a/CookBook/FirstSteps.thy Tue Feb 17 13:53:54 2009 +0000
+++ b/CookBook/FirstSteps.thy Wed Feb 18 17:17:37 2009 +0000
@@ -381,62 +381,7 @@
"Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")
$ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}
-*}
-section {* Type-Checking *}
-
-text {*
-
- You can freely construct and manipulate @{ML_type "term"}s, since they are just
- arbitrary unchecked trees. However, you eventually want to see if a
- term is well-formed, or type-checks, relative to a theory.
- Type-checking is done via the function @{ML cterm_of}, which converts
- a @{ML_type term} into a @{ML_type cterm}, a \emph{certified} term.
- Unlike @{ML_type term}s, which are just trees, @{ML_type
- "cterm"}s are abstract objects that are guaranteed to be
- type-correct, and they can only be constructed via ``official
- interfaces''.
-
- Type-checking is always relative to a theory context. For now we use
- the @{ML "@{theory}"} antiquotation to get hold of the current theory.
- For example you can write:
-
- @{ML_response_fake [display,gray] "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}
-
- This can also be written with an antiquotation:
-
- @{ML_response_fake [display,gray] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"}
-
- Attempting to obtain the certified term for
-
- @{ML_response_fake_both [display,gray] "@{cterm \"1 + True\"}" "Type unification failed \<dots>"}
-
- yields an error (since the term is not typable). A slightly more elaborate
- example that type-checks is:
-
-@{ML_response_fake [display,gray]
-"let
- val natT = @{typ \"nat\"}
- val zero = @{term \"0::nat\"}
-in
- cterm_of @{theory}
- (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero)
-end" "0 + 0"}
-
- \begin{exercise}
- Check that the function defined in Exercise~\ref{fun:revsum} returns a
- result that type-checks.
- \end{exercise}
-
- (FIXME: @{text "ctyp_of"}, @{ML fastype_of}, @{text dummyT})
-
- (FIXME: say something about constants and variables having types as
- arguments and how they can be constructed with fast-type and dummT)
-*}
-
-section {* Constants *}
-
-text {*
There are a few subtle issues with constants. They usually crop up when
pattern matching terms or constructing terms. While it is perfectly ok
to write the function @{text is_true} as follows
@@ -497,7 +442,7 @@
@{text "Nil"} is defined (@{text "List"}) and also in which datatype
(@{text "list"}). Even worse, some constants have a name involving
type-classes. Consider for example the constants for @{term "zero"}
- and @{term "(op *)"}:
+ and @{text "(op *)"}:
@{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"op *\"})"
"(Const (\"HOL.zero_class.zero\", \<dots>),
@@ -519,16 +464,17 @@
| is_nil_or_all _ = false *}
text {*
- Note that you also frequently have to calculate what the
- ``base'' name of a given constant is. For this you can use
- the function @{ML Sign.base_name}. For example:
-
- (FIXME is there an example for that statement?)
+ Note that you occasional have to calculate what the ``base'' name of a given
+ constant is. For this you can use the function @{ML Sign.extern_const} or
+ @{ML Sign.base_name}. For example:
+
+ @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""}
+ The difference between both functions is that @{ML extern_const in Sign} returns
+ the smallest name which is still unique, while @{ML base_name in Sign} always
+ strips off all qualifiers.
- @{ML_response [display,gray] "Sign.base_name \"List.list.Nil\"" "\"Nil\""}
-
- (FIXME authentic syntax?)
+ (FIXME authentic syntax on the ML-level)
\begin{readmore}
FIXME
@@ -536,14 +482,118 @@
*}
+section {* Type-Checking *}
+
+text {*
+
+ You can freely construct and manipulate @{ML_type "term"}s, since they are just
+ arbitrary unchecked trees. However, you eventually want to see if a
+ term is well-formed, or type-checks, relative to a theory.
+ Type-checking is done via the function @{ML cterm_of}, which converts
+ a @{ML_type term} into a @{ML_type cterm}, a \emph{certified} term.
+ Unlike @{ML_type term}s, which are just trees, @{ML_type
+ "cterm"}s are abstract objects that are guaranteed to be
+ type-correct, and they can only be constructed via ``official
+ interfaces''.
+
+ Type-checking is always relative to a theory context. For now we use
+ the @{ML "@{theory}"} antiquotation to get hold of the current theory.
+ For example you can write:
+
+ @{ML_response_fake [display,gray] "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}
+
+ This can also be written with an antiquotation:
+
+ @{ML_response_fake [display,gray] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"}
+
+ Attempting to obtain the certified term for
+
+ @{ML_response_fake_both [display,gray] "@{cterm \"1 + True\"}" "Type unification failed \<dots>"}
+
+ yields an error (since the term is not typable). A slightly more elaborate
+ example that type-checks is:
+
+@{ML_response_fake [display,gray]
+"let
+ val natT = @{typ \"nat\"}
+ val zero = @{term \"0::nat\"}
+in
+ cterm_of @{theory}
+ (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero)
+end" "0 + 0"}
+
+ \begin{exercise}
+ Check that the function defined in Exercise~\ref{fun:revsum} returns a
+ result that type-checks.
+ \end{exercise}
+
+ Remember that in Isabelle a term contains enough typing information
+ (constants, free variables and abstractions all have typing
+ information) so that it is always clear what the type of a term is.
+ Given a well-typed term, the function @{ML type_of} returns the
+ type of a term. Consider for example:
+
+ @{ML_response [display,gray]
+ "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
+
+ To calculate the type, this function traverses the whole term and will
+ detect any inconsistency. For examle changing the type of the variable
+ from @{typ "nat"} to @{typ "int"} will result in the error message:
+
+ @{ML_response_fake [display,gray]
+ "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})"
+ "*** Exception- TYPE (\"type_of: type mismatch in application\" \<dots>"}
+
+ Since the complete traversal might sometimes be too costly and
+ not necessary, there is also the function @{ML fastype_of} which
+ returns a type.
+
+ @{ML_response [display,gray]
+ "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
+
+ However, efficiency is gained on the expense of skiping some tests. You
+ can see this in the following example
+
+ @{ML_response [display,gray]
+ "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" "bool"}
+
+ where no error is raised.
+
+ Sometimes it is a bit inconvenient to construct a term with
+ complete typing annotations, especially in cases where the typing
+ information is redundant. A short-cut is to use the ``place-holder''
+ type @{ML "dummyT"} and then let type-inference figure out the
+ complete type. An example is as follows:
+
+ @{ML_response_fake [display,gray]
+"let
+ val term =
+ Const (@{const_name \"plus\"}, dummyT) $ @{term \"1::nat\"} $ Free (\"x\", dummyT)
+in
+ Syntax.check_term @{context} term
+end"
+ "Const (\"HOL.plus_class.plus\", \"nat \<Rightarrow> nat \<Rightarrow> nat\") $
+ Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"}
+
+ Instead of giving explicitly the type for the constant @{text "plus"} and the free
+ variable @{text "x"}, the type-inference will fill in the missing information.
+
+
+ \begin{readmore}
+ See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading,
+ checking and pretty-printing of terms are defined.
+ \end{readmore}
+*}
+
+
section {* Theorems *}
text {*
Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm}
that can only be build by going through interfaces. As a consequence, every proof
- in Isabelle is correct by construction.
+ in Isabelle is correct by construction. This follows the tradition of the LCF approach
+ \cite{GordonMilnerWadsworth79}.
- (FIXME reference LCF-philosophy)
To see theorems in ``action'', let us give a proof on the ML-level for the following
statement:
--- a/CookBook/Package/Ind_Code.thy Tue Feb 17 13:53:54 2009 +0000
+++ b/CookBook/Package/Ind_Code.thy Wed Feb 18 17:17:37 2009 +0000
@@ -19,6 +19,20 @@
@{ML_chunk [display,gray] intro_rules}
+
*}
+text {*
+ Things to include at the end:
+
+ \begin{itemize}
+ \item say something about add-inductive-i to return
+ the rules
+ \item say that the induction principle is weaker (weaker than
+ what the standard inductive package generates)
+ \end{itemize}
+
+*}
+
+
end
--- a/CookBook/Package/Ind_Examples.thy Tue Feb 17 13:53:54 2009 +0000
+++ b/CookBook/Package/Ind_Examples.thy Wed Feb 18 17:17:37 2009 +0000
@@ -306,6 +306,8 @@
qed
text {*
+ (FIXME check that the code works like as indicated)
+
The point of these examples is to get a feeling what the automatic proofs
should do in order to solve all inductive definitions we throw at them. For this
it is instructive to look at the general construction principle
--- a/CookBook/Package/Ind_Interface.thy Tue Feb 17 13:53:54 2009 +0000
+++ b/CookBook/Package/Ind_Interface.thy Wed Feb 18 17:17:37 2009 +0000
@@ -8,6 +8,25 @@
The purpose of the package we show next is that the user just specifies the
inductive predicate by stating some introduction rules and then the packages
makes the equivalent definition and derives from it the needed properties.
+*}
+
+text {*
+ From a high-level perspective the package consists of 6 subtasks:
+
+ \begin{itemize}
+ \item reading the various parts of specification (i.e.~parser),
+ \item transforming the parser outut into an internal
+ (typed) datastructure,
+ \item making the definitions,
+ \item deriving the induction principles,
+ \item deriving the introduction rules, and
+ \item storing the results in the given theory.
+ to the user.
+ \end{itemize}
+
+*}
+
+text {*
To be able to write down the specification in Isabelle, we have to introduce
a new command (see Section~\ref{sec:newcommand}). As the keyword for the new
command we chose \simpleinductive{}. The specifications corresponding to our
@@ -83,22 +102,6 @@
*}
text {*
- From a high-level perspective the package consists of 6 subtasks:
-
- \begin{itemize}
- \item reading the various parts of specification (i.e.~parser),
- \item transforming the parser outut into an internal
- (typed) datastructure,
- \item making the definitions,
- \item deriving the induction principles,
- \item deriving the introduction rules, and
- \item storing the results in the given theory to be visible
- to the user.
- \end{itemize}
-
-*}
-
-text {*
\begin{figure}[p]
\begin{isabelle}
\railnontermfont{\rmfamily\itshape}
@@ -232,7 +235,7 @@
*}
text {*
- (FIXME: explain Binding.binding; mixfix; Attrib.src; Attrib.src somewhere else)
+ (FIXME: explain Binding.binding; Attrib.binding somewhere else)
The function for external invocation of the package is called @{ML
--- a/CookBook/Package/simple_inductive_package.ML Tue Feb 17 13:53:54 2009 +0000
+++ b/CookBook/Package/simple_inductive_package.ML Wed Feb 18 17:17:37 2009 +0000
@@ -60,31 +60,31 @@
(* @chunk induction_rules *)
fun INDUCTION rules preds' Tss defs lthy1 lthy2 =
let
- val (Pnames, lthy3) = Variable.variant_fixes (replicate (length preds') "P") lthy2;
- val Ps = map (fn (s, Ts) => Free (s, Ts ---> HOLogic.boolT)) (Pnames ~~ Tss);
- val cPs = map (cterm_of (ProofContext.theory_of lthy3)) Ps;
- val rules'' = map (subst_free (preds' ~~ Ps)) rules;
+ val (Pnames, lthy3) = Variable.variant_fixes (replicate (length preds') "P") lthy2;
+ val Ps = map (fn (s, Ts) => Free (s, Ts ---> HOLogic.boolT)) (Pnames ~~ Tss);
+ val cPs = map (cterm_of (ProofContext.theory_of lthy3)) Ps;
+ val rules'' = map (subst_free (preds' ~~ Ps)) rules;
- fun prove_indrule ((R, P), Ts) =
- let
- val (znames, lthy4) = Variable.variant_fixes (replicate (length Ts) "z") lthy3;
- val zs = map Free (znames ~~ Ts)
+ fun prove_indrule ((R, P), Ts) =
+ let
+ val (znames, lthy4) = Variable.variant_fixes (replicate (length Ts) "z") lthy3;
+ val zs = map Free (znames ~~ Ts)
- val prem = HOLogic.mk_Trueprop (list_comb (R, zs))
- val goal = Logic.list_implies (rules'', HOLogic.mk_Trueprop (list_comb (P, zs)))
- in
- Goal.prove lthy4 [] [prem] goal
- (fn {prems, ...} => EVERY1
- ([ObjectLogic.full_atomize_tac,
- cut_facts_tac prems,
- K (rewrite_goals_tac defs)] @
- map (fn ct => dtac (inst_spec ct)) cPs @
- [assume_tac])) |>
- singleton (ProofContext.export lthy4 lthy1)
- end;
+ val prem = HOLogic.mk_Trueprop (list_comb (R, zs))
+ val goal = Logic.list_implies (rules'', HOLogic.mk_Trueprop (list_comb (P, zs)))
+ in
+ Goal.prove lthy4 [] [prem] goal
+ (fn {prems, ...} => EVERY1
+ ([ObjectLogic.full_atomize_tac,
+ cut_facts_tac prems,
+ K (rewrite_goals_tac defs)] @
+ map (fn ct => dtac (inst_spec ct)) cPs @
+ [assume_tac])) |>
+ singleton (ProofContext.export lthy4 lthy1)
+ end;
in
- map prove_indrule (preds' ~~ Ps ~~ Tss)
-end
+ map prove_indrule (preds' ~~ Ps ~~ Tss)
+ end
(* @end *)
(* @chunk intro_rules *)
@@ -123,22 +123,22 @@
(* @chunk add_inductive_i *)
fun add_inductive_i preds params specs lthy =
- let
- val params' = map (fn (p, T) => Free (Binding.base_name p, T)) params;
- val preds' = map (fn ((R, T), _) => list_comb (Free (Binding.base_name R, T), params')) preds;
- val Tss = map (binder_types o fastype_of) preds';
- val (ass,rules) = split_list specs;
+let
+ val params' = map (fn (p, T) => Free (Binding.base_name p, T)) params;
+ val preds' = map (fn ((R, T), _) => list_comb (Free (Binding.base_name R, T), params')) preds;
+ val Tss = map (binder_types o fastype_of) preds';
+ val (ass,rules) = split_list specs;
- val (defs, lthy1) = definitions params' rules preds preds' Tss lthy
- val (_, lthy2) = Variable.add_fixes (map (Binding.base_name o fst) params) lthy1;
+ val (defs, lthy1) = definitions params' rules preds preds' Tss lthy
+ val (_, lthy2) = Variable.add_fixes (map (Binding.base_name o fst) params) lthy1;
- val inducts = INDUCTION rules preds' Tss defs lthy1 lthy2
+ val inducts = INDUCTION rules preds' Tss defs lthy1 lthy2
- val intros = INTROS rules preds' defs lthy1 lthy2
+ val intros = INTROS rules preds' defs lthy1 lthy2
- val mut_name = space_implode "_" (map (Binding.base_name o fst o fst) preds);
- val case_names = map (Binding.base_name o fst o fst) specs
- in
+ val mut_name = space_implode "_" (map (Binding.base_name o fst o fst) preds);
+ val case_names = map (Binding.base_name o fst o fst) specs
+in
lthy1
|> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) =>
((Binding.qualify mut_name a, atts), [([th], [])])) (specs ~~ intros))
@@ -152,7 +152,7 @@
Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])]))
(preds ~~ inducts)) #>> maps snd)
|> snd
- end
+end
(* @end *)
(* @chunk read_specification *)
@@ -184,10 +184,10 @@
OuterParse.fixes --
OuterParse.for_fixes --
Scan.optional
- (OuterParse.$$$ "where" |--
- OuterParse.!!!
- (OuterParse.enum1 "|"
- (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []
+ (OuterParse.$$$ "where" |--
+ OuterParse.!!!
+ (OuterParse.enum1 "|"
+ (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []
(* @end *)
(* @chunk syntax *)
--- a/CookBook/Parsing.thy Tue Feb 17 13:53:54 2009 +0000
+++ b/CookBook/Parsing.thy Wed Feb 18 17:17:37 2009 +0000
@@ -528,7 +528,7 @@
text {*
There are a number of special purpose parsers that help with parsing
- specifications for functions, inductive definitions and so on. In
+ specifications of functions, inductive definitions and so on. In
Capter~\ref{chp:package}, for example, we will need to parse specifications
for inductive predicates of the form:
*}
@@ -555,13 +555,15 @@
OuterParse.fixes --
OuterParse.for_fixes --
Scan.optional
- (OuterParse.$$$ "where" |--
- OuterParse.!!!
- (OuterParse.enum1 "|"
- (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
+ (OuterParse.$$$ "where" |--
+ OuterParse.!!!
+ (OuterParse.enum1 "|"
+ (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
text {*
- To see what it returns, let us parse the string corresponding to the
+ Note that the parser does not parse the ketword \simpleinductive. This
+ will be done by the infrastructure that will eventually call this parser.
+ To see what the parser returns, let us parse the string corresponding to the
definition of @{term even} and @{term odd}:
@{ML_response [display,gray]
@@ -581,7 +583,7 @@
((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"}
As can be seen, the result is a ``nested'' four-tuple consisting of an
- optional locale; a list of variables with optional type-annotation and optional
+ optional locale; a list of variables with optional type-annotation and
syntax-annotation; a list of for-fixes (fixed variables); and a list of rules
where each rule has optionally a name and an attribute.
@@ -591,10 +593,11 @@
@{ML_response [display,gray]
"parse OuterParse.opt_target (filtered_input \"(in test)\")" "(SOME \"test\",[])"}
- The function @{ML OuterParse.opt_target} returns @{ML NONE}, if no target is given.
+ returns the locale @{text [quotes] "test"}; if no target is given' like in the
+ casde of @{text "even"} and @{text "odd"}, the function returns @{ML NONE}.
The function @{ML OuterParse.fixes} in Line 3 reads an \isacommand{and}-separated
- list of variables that can include type annotations and syntax translations.
+ list of variables that can include optional type annotations and syntax translations.
For example:\footnote{Note that in the code we need to write
@{text "\\\"int \<Rightarrow> bool\\\""} in order to properly escape the double quotes
in the compound type.}
@@ -613,7 +616,8 @@
text {*
Whenever types are given, they are stored in the @{ML SOME}s. Since types
- are part of the inner syntax they are strings with some printing directives.
+ are part of the inner syntax they are strings with some printing directives
+ (see previous section).
If a syntax translation is present for a variable, then it is
stored in the @{ML Mixfix} datastructure; no syntax translation is
indicated by @{ML NoSyn}.
@@ -627,10 +631,10 @@
but requires that this list is prefixed by the keyword \isacommand{for}.
@{ML_response [display,gray]
-"parse OuterParse.for_fixes (filtered_input \"for foo and bar\")"
-"([(foo, NONE, NoSyn), (bar, NONE, NoSyn)],[])"}
+"parse OuterParse.for_fixes (filtered_input \"for foo and bar and blink\")"
+"([(foo, NONE, NoSyn), (bar, NONE, NoSyn), (blink, NONE, NoSyn)],[])"}
- Lines 5 to 9 include the parser for a list of introduction rules, that is propositions
+ Lines 5 to 9 implement the parser for a list of introduction rules, that is propositions
with theorem annotations. The introduction rules are propositions parsed
by @{ML OuterParse.prop}. However, they can include an optional theorem name plus
some attributes. For example
@@ -642,16 +646,20 @@
(name, map Args.dest_src attrib)
end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"}
+ A name of a theorem can be quite complicated, as it can include attrinutes.
The function @{ML opt_thm_name in SpecParse} is the ``optional'' variant of
@{ML thm_name in SpecParse}. As can be seen each theorem name can contain some
attributes. If you want to print out all currently known attributes a theorem
can have, you can use the function:
-*}
-ML{*Attrib.print_attributes @{theory}*}
+ @{ML_response_fake [display,gray] "Attrib.print_attributes @{theory}"
+"COMP: direct composition with rules (no lifting)
+HOL.dest: declaration of Classical destruction rule
+HOL.elim: declaration of Classical elimination rule
+\<dots>"}
-text {*
- For the inductive definitions described above only the attibutes @{text "[intro]"} and
+
+ For the inductive definitions described above only, the attibutes @{text "[intro]"} and
@{text "[simp]"} make sense.
\begin{readmore}
--- a/CookBook/document/root.bib Tue Feb 17 13:53:54 2009 +0000
+++ b/CookBook/document/root.bib Wed Feb 18 17:17:37 2009 +0000
@@ -1,6 +1,6 @@
@Misc{Bornat-lecture,
- author = {Richard Bornat},
- title = {In defence of programming},
+ author = {R.~Bornat},
+ title = {In {D}efence of {P}rogramming},
howpublished = {Available online via
\url{http://www.cs.mdx.ac.uk/staffpages/r_bornat/lectures/ revisedinauguraltext.pdf}},
month = {April},
@@ -11,7 +11,7 @@
}
@inproceedings{Krauss-IJCAR06,
- author = {Alexander Krauss},
+ author = {A.~Krauss},
title = {{P}artial {R}ecursive {F}unctions in {H}igher-{O}rder {L}ogic},
editor = {Ulrich Furbach and Natarajan Shankar},
booktitle = {Automated Reasoning, Third International Joint
@@ -25,7 +25,7 @@
}
@INPROCEEDINGS{Melham:1992:PIR,
- AUTHOR = {T. F. Melham},
+ AUTHOR = {T.~F.~Melham},
TITLE = {{A} {P}ackage for {I}nductive {R}elation {D}efinitions in
{HOL}},
BOOKTITLE = {Proceedings of the 1991 International Workshop on
@@ -41,7 +41,7 @@
}
@Book{isa-tutorial,
- author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
+ author = {T.~Nipkow and L.~C.~Paulson and M.~Wenzel},
title = {Isabelle/HOL: A Proof Assistant for Higher-Order Logic},
publisher = {Springer},
year = 2002,
@@ -55,7 +55,7 @@
publisher = {Cambridge University Press}}
@InCollection{Paulson-ind-defs,
- author = {L. C. Paulson},
+ author = {L.~C.~Paulson},
title = {A fixedpoint approach to (co)inductive and
(co)datatype definitions},
booktitle = {Proof, Language, and Interaction: Essays in Honour
@@ -67,7 +67,7 @@
}
@inproceedings{Schirmer-LPAR04,
- author = {Norbert Schirmer},
+ author = {N.~Schirmer},
title = {{A} {V}erification {E}nvironment for {S}equential {I}mperative
Programs in {I}sabelle/{HOL}},
booktitle = "Logic for Programming, Artificial Intelligence, and
@@ -81,7 +81,7 @@
}
@TechReport{Schwichtenberg-MLCF,
- author = {Helmut Schwichtenberg},
+ author = {H.~Schwichtenberg},
title = {{M}inimal {L}ogic {f}or {C}omputable {F}unctionals},
institution = {Mathematisches Institut,
Ludwig-Maximilians-Universit{\"a}t M{\"u}nchen},
@@ -92,7 +92,7 @@
}
@inproceedings{Urban-Berghofer06,
- author = {Christian Urban and Stefan Berghofer},
+ author = {C.~Urban and S.~Berghofer},
title = {{A} {R}ecursion {C}ombinator for {N}ominal {D}atatypes
{I}mplemented in {I}sabelle/{HOL}},
editor = {Ulrich Furbach and Natarajan Shankar},
@@ -107,7 +107,7 @@
}
@inproceedings{Wadler-AFP95,
- author = {Philip Wadler},
+ author = {P.~Wadler},
title = {Monads for Functional Programming},
pages = {24-52},
editor = {Johan Jeuring and Erik Meijer},
@@ -122,7 +122,17 @@
}
@manual{isa-imp,
- author = {Makarius Wenzel},
+ author = {M.~Wenzel},
title = {The {Isabelle/Isar} Implementation},
institution = {Technische Universit\"at M\"unchen},
note = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}}
+
+
+@book{GordonMilnerWadsworth79,
+ author = {M.~Gordon and R.~Milner and C.~P.~Wadsworth},
+ title = {{E}dinburgh {LCF}},
+ publisher = {Springer},
+ series = {Lecture Notes in Computer Science},
+ volume = {78},
+ year = {1979}
+}
\ No newline at end of file
Binary file cookbook.pdf has changed