--- a/doc-src/IsarImplementation/Makefile Mon Feb 16 21:04:15 2009 +0100
+++ b/doc-src/IsarImplementation/Makefile Mon Feb 16 21:23:33 2009 +0100
@@ -8,8 +8,6 @@
include ../Makefile.in
-MAKEGLOSSARY = ./makeglossary
-
NAME = implementation
FILES = implementation.tex Thy/document/Prelim.tex \
@@ -26,7 +24,6 @@
$(BIBTEX) $(NAME)
$(LATEX) $(NAME)
$(LATEX) $(NAME)
- $(MAKEGLOSSARY) $(NAME)
$(SEDINDEX) $(NAME)
$(LATEX) $(NAME)
$(LATEX) $(NAME)
@@ -38,7 +35,6 @@
$(BIBTEX) $(NAME)
$(PDFLATEX) $(NAME)
$(PDFLATEX) $(NAME)
- $(MAKEGLOSSARY) $(NAME)
$(SEDINDEX) $(NAME)
$(FIXBOOKMARKS) $(NAME).out
$(PDFLATEX) $(NAME)
--- a/doc-src/IsarImplementation/Thy/Logic.thy Mon Feb 16 21:04:15 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/Logic.thy Mon Feb 16 21:23:33 2009 +0100
@@ -186,12 +186,9 @@
*}
-
section {* Terms \label{sec:terms} *}
text {*
- \glossary{Term}{FIXME}
-
The language of terms is that of simply-typed @{text "\<lambda>"}-calculus
with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}
or \cite{paulson-ml2}), with the types being determined determined
@@ -392,42 +389,6 @@
section {* Theorems \label{sec:thms} *}
text {*
- \glossary{Proposition}{FIXME A \seeglossary{term} of
- \seeglossary{type} @{text "prop"}. Internally, there is nothing
- special about propositions apart from their type, but the concrete
- syntax enforces a clear distinction. Propositions are structured
- via implication @{text "A \<Longrightarrow> B"} or universal quantification @{text
- "\<And>x. B x"} --- anything else is considered atomic. The canonical
- form for propositions is that of a \seeglossary{Hereditary Harrop
- Formula}. FIXME}
-
- \glossary{Theorem}{A proven proposition within a certain theory and
- proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
- rarely spelled out explicitly. Theorems are usually normalized
- according to the \seeglossary{HHF} format. FIXME}
-
- \glossary{Fact}{Sometimes used interchangeably for
- \seeglossary{theorem}. Strictly speaking, a list of theorems,
- essentially an extra-logical conjunction. Facts emerge either as
- local assumptions, or as results of local goal statements --- both
- may be simultaneous, hence the list representation. FIXME}
-
- \glossary{Schematic variable}{FIXME}
-
- \glossary{Fixed variable}{A variable that is bound within a certain
- proof context; an arbitrary-but-fixed entity within a portion of
- proof text. FIXME}
-
- \glossary{Free variable}{Synonymous for \seeglossary{fixed
- variable}. FIXME}
-
- \glossary{Bound variable}{FIXME}
-
- \glossary{Variable}{See \seeglossary{schematic variable},
- \seeglossary{fixed variable}, \seeglossary{bound variable}, or
- \seeglossary{type variable}. The distinguishing feature of
- different variables is their binding scope. FIXME}
-
A \emph{proposition} is a well-typed term of type @{text "prop"}, a
\emph{theorem} is a proven proposition (depending on a context of
hypotheses and the background theory). Primitive inferences include
@@ -436,6 +397,7 @@
notion of equality/equivalence @{text "\<equiv>"}.
*}
+
subsection {* Primitive connectives and rules \label{sec:prim-rules} *}
text {*
@@ -801,16 +763,13 @@
expect a normal form: quantifiers @{text "\<And>"} before implications
@{text "\<Longrightarrow>"} at each level of nesting.
-\glossary{Hereditary Harrop Formula}{The set of propositions in HHF
-format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>
-A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.
-Any proposition may be put into HHF form by normalizing with the rule
-@{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}. In Isabelle, the outermost
-quantifier prefix is represented via \seeglossary{schematic
-variables}, such that the top-level structure is merely that of a
-\seeglossary{Horn Clause}}.
-
-\glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}
+ The set of propositions in HHF format is defined inductively as
+ @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow> A)"}, for variables @{text "x"}
+ and atomic propositions @{text "A"}. Any proposition may be put
+ into HHF form by normalizing with the rule @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv>
+ (\<And>x. A \<Longrightarrow> B x)"}. In Isabelle, the outermost quantifier prefix is
+ represented via schematic variables, such that the top-level
+ structure is merely that of a Horn Clause.
\[
--- a/doc-src/IsarImplementation/Thy/Prelim.thy Mon Feb 16 21:04:15 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy Mon Feb 16 21:23:33 2009 +0100
@@ -74,8 +74,6 @@
subsection {* Theory context \label{sec:context-theory} *}
text {*
- \glossary{Theory}{FIXME}
-
A \emph{theory} is a data container with explicit named and unique
identifier. Theories are related by a (nominal) sub-theory
relation, which corresponds to the dependency graph of the original
@@ -201,13 +199,6 @@
subsection {* Proof context \label{sec:context-proof} *}
text {*
- \glossary{Proof context}{The static context of a structured proof,
- acts like a local ``theory'' of the current portion of Isar proof
- text, generalizes the idea of local hypotheses @{text "\<Gamma>"} in
- judgments @{text "\<Gamma> \<turnstile> \<phi>"} of natural deduction calculi. There is a
- generic notion of introducing and discharging hypotheses.
- Arbritrary auxiliary context data may be adjoined.}
-
A proof context is a container for pure data with a back-reference
to the theory it belongs to. The @{text "init"} operation creates a
proof context from a given theory. Modifications to draft theories
@@ -231,7 +222,7 @@
context is extended consecutively, and results are exported back
into the original context. Note that the Isar proof states model
block-structured reasoning explicitly, using a stack of proof
- contexts internally, cf.\ \secref{sec:isar-proof-state}.
+ contexts internally.
*}
text %mlref {*
@@ -418,10 +409,6 @@
subsection {* Strings of symbols *}
text {*
- \glossary{Symbol}{The smallest unit of text in Isabelle, subsumes
- plain ASCII characters as well as an infinite collection of named
- symbols (for greek, math etc.).}
-
A \emph{symbol} constitutes the smallest textual unit in Isabelle
--- raw characters are normally not encountered at all. Isabelle
strings consist of a sequence of symbols, represented as a packed
@@ -465,8 +452,8 @@
link to the standard collection of Isabelle.
\medskip Output of Isabelle symbols depends on the print mode
- (\secref{FIXME}). For example, the standard {\LaTeX} setup of the
- Isabelle document preparation system would present
+ (\secref{print-mode}). For example, the standard {\LaTeX} setup of
+ the Isabelle document preparation system would present
``\verb,\,\verb,<alpha>,'' as @{text "\<alpha>"}, and
``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as @{text
"\<^bold>\<alpha>"}.
--- a/doc-src/IsarImplementation/Thy/Tactic.thy Mon Feb 16 21:04:15 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/Tactic.thy Mon Feb 16 21:23:33 2009 +0100
@@ -18,21 +18,14 @@
section {* Goals \label{sec:tactical-goals} *}
text {*
- Isabelle/Pure represents a goal\glossary{Tactical goal}{A theorem of
- \seeglossary{Horn Clause} form stating that a number of subgoals
- imply the main conclusion, which is marked as a protected
- proposition.} as a theorem stating that the subgoals imply the main
- goal: @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}. The outermost goal
- structure is that of a Horn Clause\glossary{Horn Clause}{An iterated
- implication @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}, without any
- outermost quantifiers. Strictly speaking, propositions @{text
- "A\<^sub>i"} need to be atomic in Horn Clauses, but Isabelle admits
- arbitrary substructure here (nested @{text "\<Longrightarrow>"} and @{text "\<And>"}
- connectives).}: i.e.\ an iterated implication without any
- quantifiers\footnote{Recall that outermost @{text "\<And>x. \<phi>[x]"} is
- always represented via schematic variables in the body: @{text
- "\<phi>[?x]"}. These variables may get instantiated during the course of
- reasoning.}. For @{text "n = 0"} a goal is called ``solved''.
+ Isabelle/Pure represents a goal as a theorem stating that the
+ subgoals imply the main goal: @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow>
+ C"}. The outermost goal structure is that of a Horn Clause: i.e.\
+ an iterated implication without any quantifiers\footnote{Recall that
+ outermost @{text "\<And>x. \<phi>[x]"} is always represented via schematic
+ variables in the body: @{text "\<phi>[?x]"}. These variables may get
+ instantiated during the course of reasoning.}. For @{text "n = 0"}
+ a goal is called ``solved''.
The structure of each subgoal @{text "A\<^sub>i"} is that of a general
Hereditary Harrop Formula @{text "\<And>x\<^sub>1 \<dots> \<And>x\<^sub>k. H\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> H\<^sub>m \<Longrightarrow> B"} in
@@ -45,14 +38,9 @@
exceeds 1--2 in practice.
The main conclusion @{text C} is internally marked as a protected
- proposition\glossary{Protected proposition}{An arbitrarily
- structured proposition @{text "C"} which is forced to appear as
- atomic by wrapping it into a propositional identity operator;
- notation @{text "#C"}. Protecting a proposition prevents basic
- inferences from entering into that structure for the time being.},
- which is represented explicitly by the notation @{text "#C"}. This
- ensures that the decomposition into subgoals and main conclusion is
- well-defined for arbitrarily structured claims.
+ proposition, which is represented explicitly by the notation @{text
+ "#C"}. This ensures that the decomposition into subgoals and main
+ conclusion is well-defined for arbitrarily structured claims.
\medskip Basic goal management is performed via the following
Isabelle/Pure rules:
@@ -405,14 +393,12 @@
section {* Tacticals \label{sec:tacticals} *}
text {*
-
-FIXME
+ A \emph{tactical} is a functional combinator for building up complex
+ tactics from simpler ones. Typical tactical perform sequential
+ composition, disjunction (choice), iteration, or goal addressing.
+ Various search strategies may be expressed via tacticals.
-\glossary{Tactical}{A functional combinator for building up complex
-tactics from simpler ones. Typical tactical perform sequential
-composition, disjunction (choice), iteration, or goal addressing.
-Various search strategies may be expressed via tacticals.}
-
+ \medskip FIXME
*}
end
--- a/doc-src/IsarImplementation/checkglossary Mon Feb 16 21:04:15 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-#!/usr/bin/env perl
-# $Id$
-
-use strict;
-
-my %defs = ();
-my %refs = ();
-
-while (<ARGV>) {
- if (m,\\glossaryentry\{\w*\\bf *((\w|\s)+)@,) {
- $defs{lc $1} = 1;
- }
- while (m,\\seeglossary *\{((\w|\s)+)\},g) {
- $refs{lc $1} = 1;
- }
-}
-
-print "Glossary definitions:\n";
-foreach (sort(keys(%defs))) {
- print " \"$_\"\n";
-}
-
-foreach (keys(%refs)) {
- s,s$,,;
- if (!defined($defs{$_})) {
- print "### Undefined glossary reference: \"$_\"\n";
- }
-}
--- a/doc-src/IsarImplementation/implementation.tex Mon Feb 16 21:04:15 2009 +0100
+++ b/doc-src/IsarImplementation/implementation.tex Mon Feb 16 21:23:33 2009 +0100
@@ -20,9 +20,6 @@
and Larry Paulson
}
-%FIXME
-%\makeglossary
-
\makeindex
@@ -85,10 +82,6 @@
\bibliography{../manual}
\endgroup
-%FIXME
-%\tocentry{\glossaryname}
-%\printglossary
-
\tocentry{\indexname}
\printindex
--- a/doc-src/IsarImplementation/makeglossary Mon Feb 16 21:04:15 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-#!/bin/sh
-# $Id$
-
-NAME="$1"
-makeindex -s nomencl -o "${NAME}.gls" "${NAME}.glo"
-./checkglossary "${NAME}.glo"
--- a/doc-src/IsarImplementation/style.sty Mon Feb 16 21:04:15 2009 +0100
+++ b/doc-src/IsarImplementation/style.sty Mon Feb 16 21:23:33 2009 +0100
@@ -1,6 +1,3 @@
-
-%% $Id$
-
%% toc
\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
@@ -10,13 +7,6 @@
\newcommand{\chref}[1]{chapter~\ref{#1}}
\newcommand{\figref}[1]{figure~\ref{#1}}
-%% glossary
-\renewcommand{\glossary}[2]{\nomenclature{\bf #1}{#2}}
-\newcommand{\seeglossary}[1]{\emph{#1}}
-\newcommand{\glossaryname}{Glossary}
-\renewcommand{\nomname}{\glossaryname}
-\renewcommand{\pagedeclaration}[1]{\nobreak\quad\dotfill~page~\bold{#1}}
-
%% index
\newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
\newcommand{\indexmlexception}[1]{\index{\emph{#1} (exception)|bold}}
@@ -61,6 +51,7 @@
\isabellestyle{it}
+
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "implementation"