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