tuned message;

changed the index sort key from |-| to just |- because pdflatex can't cope with the two ||s in the index entry

HOL-Hyperreal produces an image (again);

dependencies for "typedef" image;

improved arrangement of "typedef" images;

no_document use_thy "While_Combinator";

tuned;

tuned;

tuned;

updated;

tuned;

\part{Elementary Techniques};

\chapter{The Basics};

Added some simprules proofs. Converted theories CardinalArith and OrdQuant to Isar style

updated;

tuned;

added filter_filter

#2 to 2

syntax "_not_equal";

removed (not really necessary, causes too many consistency problems);

tuned;

getting close to completion;

updated;

tuned;

updated;

tuned;

tuned deps;

tuned;

updated;

some more ...;

"_not_equal" dummy constant;

updated;

some more text;

updated;

tuned;

some text on document preparation;

updated;

tuned;

updated;

mention X-Symbol; \index{Aspinall, David};

updated;

use wasysym package;

\newcommand{\isasymignore}{}, so we may use \<ignore> to disambiguate duplicate syntax declarations for demonstration purposes;

tuned;

\hfootref: use \url markup;

more on concrete syntax;

fixed \index;

tuned ``syntax (output)'';

isatool document: stderr to stdout;

tuned;

document preparation overview;

beginnings of concrete syntax;

include typedef image without path prefix!

updated;

link Types/typedef images;

Isar version; support constdefs, too;

tuned msg;

\CONSTDEFS;

tuned;

next round of updates;