--- a/doc-src/IsarImplementation/Thy/Logic.thy Mon Jun 06 18:05:38 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/Logic.thy Mon Jun 06 19:08:46 2011 +0200
@@ -366,6 +366,7 @@
@{index_ML fastype_of: "term -> typ"} \\
@{index_ML lambda: "term -> term -> term"} \\
@{index_ML betapply: "term * term -> term"} \\
+ @{index_ML incr_boundvars: "int -> term -> term"} \\
@{index_ML Sign.declare_const: "Proof.context ->
(binding * typ) * mixfix -> theory -> term * theory"} \\
@{index_ML Sign.add_abbrev: "string -> binding * term ->
@@ -414,6 +415,12 @@
"t u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} is an
abstraction.
+ \item @{ML incr_boundvars}~@{text "j"} increments a term's dangling
+ bound variables by the offset @{text "j"}. This is required when
+ moving a subterm into a context where it is enclosed by a different
+ number of abstractions. Bound variables with a matching abstraction
+ are unaffected.
+
\item @{ML Sign.declare_const}~@{text "ctxt ((c, \<sigma>), mx)"} declares
a new constant @{text "c :: \<sigma>"} with optional mixfix syntax.
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex Mon Jun 06 18:05:38 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Mon Jun 06 19:08:46 2011 +0200
@@ -404,6 +404,7 @@
\indexdef{}{ML}{fastype\_of}\verb|fastype_of: term -> typ| \\
\indexdef{}{ML}{lambda}\verb|lambda: term -> term -> term| \\
\indexdef{}{ML}{betapply}\verb|betapply: term * term -> term| \\
+ \indexdef{}{ML}{incr\_boundvars}\verb|incr_boundvars: int -> term -> term| \\
\indexdef{}{ML}{Sign.declare\_const}\verb|Sign.declare_const: Proof.context ->|\isasep\isanewline%
\verb| (binding * typ) * mixfix -> theory -> term * theory| \\
\indexdef{}{ML}{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> binding * term ->|\isasep\isanewline%
@@ -444,6 +445,12 @@
\item \verb|betapply|~\isa{{\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ u{\isaliteral{29}{\isacharparenright}}} produces an application \isa{t\ u}, with topmost \isa{{\isaliteral{5C3C626574613E}{\isasymbeta}}}-conversion if \isa{t} is an
abstraction.
+ \item \verb|incr_boundvars|~\isa{j} increments a term's dangling
+ bound variables by the offset \isa{j}. This is required when
+ moving a subterm into a context where it is enclosed by a different
+ number of abstractions. Bound variables with a matching abstraction
+ are unaffected.
+
\item \verb|Sign.declare_const|~\isa{ctxt\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ mx{\isaliteral{29}{\isacharparenright}}} declares
a new constant \isa{c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} with optional mixfix syntax.
--- a/doc-src/Ref/Makefile Mon Jun 06 18:05:38 2011 +0200
+++ b/doc-src/Ref/Makefile Mon Jun 06 19:08:46 2011 +0200
@@ -10,7 +10,7 @@
NAME = ref
FILES = ref.tex introduction.tex tactic.tex tctical.tex thm.tex \
- theories.tex defining.tex syntax.tex substitution.tex \
+ defining.tex syntax.tex substitution.tex \
simplifier.tex classical.tex ../proof.sty ../iman.sty \
../extra.sty ../ttbox.sty ../manual.bib
--- a/doc-src/Ref/ref.tex Mon Jun 06 18:05:38 2011 +0200
+++ b/doc-src/Ref/ref.tex Mon Jun 06 19:08:46 2011 +0200
@@ -36,11 +36,9 @@
\subsubsection*{Acknowledgements}
Tobias Nipkow, of T. U. Munich, wrote most of
- Chapters~\protect\ref{Defining-Logics} and~\protect\ref{chap:simplification},
- and part of
- Chapter~\protect\ref{theories}. Carsten Clasohm also contributed to
- Chapter~\protect\ref{theories}. Markus Wenzel contributed to
- Chapter~\protect\ref{chap:syntax}. Jeremy Dawson, Sara Kalvala, Martin
+ Chapters~\protect\ref{Defining-Logics} and~\protect\ref{chap:simplification}.
+ Markus Wenzel contributed to Chapter~\protect\ref{chap:syntax}.
+ Jeremy Dawson, Sara Kalvala, Martin
Simons and others suggested changes
and corrections. The research has been funded by the EPSRC (grants
GR/G53279, GR/H40570, GR/K57381, GR/K77051, GR/M75440) and by ESPRIT
@@ -53,7 +51,6 @@
\include{tactic}
\include{tctical}
\include{thm}
-\include{theories}
\include{defining}
\include{syntax}
\include{substitution}
--- a/doc-src/Ref/theories.tex Mon Jun 06 18:05:38 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,44 +0,0 @@
-
-\chapter{Terms}
-
-\section{*Variable binding}
-\begin{ttbox}
-loose_bnos : term -> int list
-incr_boundvars : int -> term -> term
-abstract_over : term*term -> term
-variant_abs : string * typ * term -> string * term
-\end{ttbox}
-These functions are all concerned with the de Bruijn representation of
-bound variables.
-\begin{ttdescription}
-\item[\ttindexbold{loose_bnos} $t$]
- returns the list of all dangling bound variable references. In
- particular, \texttt{Bound~0} is loose unless it is enclosed in an
- abstraction. Similarly \texttt{Bound~1} is loose unless it is enclosed in
- at least two abstractions; if enclosed in just one, the list will contain
- the number 0. A well-formed term does not contain any loose variables.
-
-\item[\ttindexbold{incr_boundvars} $j$]
- increases a term's dangling bound variables by the offset~$j$. This is
- required when moving a subterm into a context where it is enclosed by a
- different number of abstractions. Bound variables with a matching
- abstraction are unaffected.
-
-\item[\ttindexbold{abstract_over} $(v,t)$]
- forms the abstraction of~$t$ over~$v$, which may be any well-formed term.
- It replaces every occurrence of \(v\) by a \texttt{Bound} variable with the
- correct index.
-
-\item[\ttindexbold{variant_abs} $(a,T,u)$]
- substitutes into $u$, which should be the body of an abstraction.
- It replaces each occurrence of the outermost bound variable by a free
- variable. The free variable has type~$T$ and its name is a variant
- of~$a$ chosen to be distinct from all constants and from all variables
- free in~$u$.
-
-\end{ttdescription}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "ref"
-%%% End: