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;