Branch: top elements of stack only need to be convertible (not equal)

tuned;

-I option;

-D PATH: dump generated document sources into PATH;

additional tex dump;

'.' == by this;

misc improvements;

added MicroJava/document;

added old_symbol_source; tuned;

Present.old_symbol_source;

tuned;

manually load session;

tuned syms;

new theorem gcd_add_mult

most_general_varify_tfrees all results;

Rduced Class C <= Class D to C <= D.

nat as names; obtain; tuned;

expandshort

new lemma fun_cons_restrict_eq

new theorems by Sidi O. Ehmety

added forgotten definition of make_imp_tac

added forgotten rules to make IMPP

eliminated nonascii;

added IMPP to HOL

renamed image_Union_eq -> image_Union

new theorem vimage_Union

new theorem rev_ImageI

various theorems about image and inverse image

Pi_empty1 is a more general simprule than empty_fun

rm -f *.aux;

simp_all method;

eliminated proof script;

HEADGOAL;

added prefer, defer;

added HEADGOAL;

added defer, prefer;

Drule.instantiate;

cp -r;

-p option;

added range_composition (also to simpset)

added finite_range_updI, finite_range_map_of, finite_range_map_of_override added, also to simpset: override_upd, ran_empty'

mkdir: prepare logic session directory;

added full_nat_induct

added splitE', also to claset

added inj_singleton

added finite_range_imageI

replaced FIRSTGOAL by FINDGOAL (backtracking!);

maintain standard rules (beware: classical provers provides another version!);

replaced FIRSTGOAL by FINDGOAL (backtracking!); improved flexflex handling; tuned sig;

tuned sig;

map data;

added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED

beautified spacing for binders with symbols syntax, analogous to HOL.thy

*** empty log message ***

'name' etc. include 'number'; attrib: include keyword_sid as name;

'name' syntax includes numbers;

optimized xs[i:=x]!j lemmas.

added map, map_st;

added map;

fallback on PureThy version;