* system: reduced base memory usage by Poly/ML (approx. 20 MB instead of 40 MB), cf. ML_OPTIONS;

ML_OPTIONS="-h 15000" (used to be 30000);

updated;

tuned;

updated;

tuned;

updated;

tuned;

updated;

tuned;

tuned;

cosmetics

\<twosuperior> syntax moved to HOL/Numerals;

tuned;

prime_dvd_power_two;

symbolic syntax for x^2 (faills back on plain infix "^");

\usepackage[latin1]{inputenc};

* HOL: symbolic syntax for x^2 (numeral 2);

added HOL/Real/document/root.tex;

HOL-Real/Complex_Numbers;

Real/Complex_Numbers.thy;

tuned;

tuned;

produce predicate text; proper checking of defines;

added atomize_cterm;

tuned;

unify_frozen: proper use of maxidx'; declare_elemss: need to unify_elemss beforehand;

paramify_dummies: proper treatment of maxidx;

renamed forall_elim_vars_safe to gen_all;

Isabelle2002 (January 2002);

removed obsolete isamode.ML;

tuned;

#!/usr/bin/env bash;

replace gen_all by forall_elim_vars_safe;

improved forall_elim_vars_safe (no longer invents new indexes);

lemmas (in ACe) AC;

tuned;

IsarThy.theorems_i;

moved setmksimps to Main!

have_thmss vs. have_thmss_i; with_thmss vs. with_thmss_i;

clarified/added theorems(_i) vs. locale_theorems(_i); clarified IsarThy.apply_theorems_i; localized smart_theorems, declare_theorems; removed declare_theorems_i;

localized 'lemmas', 'theorems', 'declare';

have_thmss vs. have_thmss_i;

kind: ignore "";

IsarThy.theorems_i;

clarified IsarThy.apply_theorems_i;

* Pure: localized 'lemmas', 'theorems', 'declare';

removed add_thmss; added have_thmss(_i);

tuned;

export_single;

refine_tac: Tactic.norm_hhf_tac before trying rule; global_qed: uses Locale.add_thmss_hybrid, tuned;

add_thmss_hybrid;

export multi_theorem(_i), locale_multi_theorem(_i);

stylistic changes

*** empty log message ***

locales: hide base name of exported version;

simplified theorem(_i); smart_multi_theorem;

IsarThy.smart_multi_theorem;

added hide_thms;

simplified IsarThy.theorem_i;

qualified exports from locales;

obsolete;

converted theory Transitive_Closure;

* added \<euro> symbol; * HOL-Hyperreal is now a logic image; * isatool latex no longer depends on changed TEXINPUTS;

no longer requires TEXINPUTS;

isatool latex -o sty;

removed TEXINPUTS;

updated;

tuned;

updated;

tuned;

updated;

tuned;

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;