isabelle: Changelog

haftmann [Tue, 07 Jul 2009 17:21:26 +0200] rev 31956

more accurate certificates for constant aliasses

haftmann [Tue, 07 Jul 2009 21:24:55 +0200] rev 31955

merged

haftmann [Tue, 07 Jul 2009 17:37:00 +0200] rev 31954

Stefan Berghofer's code generator uses Pure equality instead of HOL equality now

wenzelm [Tue, 07 Jul 2009 20:16:06 +0200] rev 31953

fixed proof (cf. 40501bb2d57c);

nipkow [Tue, 07 Jul 2009 17:39:51 +0200] rev 31952

renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int

haftmann [Tue, 07 Jul 2009 07:56:24 +0200] rev 31951

merged

haftmann [Mon, 06 Jul 2009 16:49:51 +0200] rev 31950

tuned code

haftmann [Mon, 06 Jul 2009 14:19:13 +0200] rev 31949

moved Inductive.myinv to Fun.inv; tuned

wenzelm [Tue, 07 Jul 2009 00:29:34 +0200] rev 31948

add_classrel/arity: strip_shyps of stored result;

wenzelm [Mon, 06 Jul 2009 22:42:27 +0200] rev 31947

clarified strip_shyps: proper type witnesses for present sorts; moved fold_terms to thm.ML;

isabelle