generate table of isabelle symbols;

removed Digest (temporarily, not up to date) added theory JVM

updated for is_class changes

removed two intermediate comments

fixed and cleaned up wt[l]_jvm_prog proofs

tuned;

update for changes in Correct.thy and class/is_class defs

strengthened invariant: current class must be defined

update for changes in Step.thy

invoked class must be defined in Invoke C ...

unsymbolize;

left_minus axiom;

tuned;

activate Rational_Numbers;

deactivate Rational_Numbers (tmp!);

updated;

Rational_Numbers;

less rude treatment of "no_def";

added Library/Rational_Numbers.thy;

improved superclass entry for classes and definition status of is_class, class corrected recursive definitions of "method" and "fields" cleanup of many proofs, removed superfluous tactics and theorems

improved superclass entry for classes and definition status of is_class, class corrected recursive definitions of "method" and "fields" Beware: some proofs are incomplete (sorry, oops), preliminary comments with DvO:

simplified interactive handling

some derived properties;

HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse" function;

*** empty log message ***

converted rinv and hrinv to inverse;

converted rinv to inverse;

added \<a> ... \<z>;

tuned;

theory file for Numbers section