isabelle: Changelog

wenzelm [Tue, 08 Aug 2000 16:57:44 +0200] rev 9558

token translation: enclose "\\mbox{" "}";

oheimb [Tue, 08 Aug 2000 16:39:34 +0200] rev 9557

added Example

oheimb [Tue, 08 Aug 2000 14:15:24 +0200] rev 9556

moved Hoare_example to Examples; other minor improvements

berghofe [Tue, 08 Aug 2000 13:23:45 +0200] rev 9555

Deleted unneeded proof; simplified proof of app_last.

wenzelm [Tue, 08 Aug 2000 01:26:34 +0200] rev 9554

added forall_elim_vars_safe, norm_hhf_eq;

wenzelm [Tue, 08 Aug 2000 01:17:59 +0200] rev 9553

norm_hhf results;

wenzelm [Tue, 08 Aug 2000 01:17:28 +0200] rev 9552

prf_heading kind;

kleing [Mon, 07 Aug 2000 14:34:26 +0200] rev 9551

MicroJava structure changed

kleing [Mon, 07 Aug 2000 14:34:03 +0200] rev 9550

Invoke instruction gets fully qualified method name (class+name+sig) as in Sun's JVM spec

kleing [Mon, 07 Aug 2000 14:32:56 +0200] rev 9549

BV and LBV specified in terms of app and step functions

isabelle