paulson [Fri, 02 Feb 2001 11:42:36 +0100] rev 11030
new theorem fib_mult_eq_setsum
oheimb [Fri, 02 Feb 2001 00:31:39 +0100] rev 11029
little bugfixes; added induct_thm_tac
wenzelm [Thu, 01 Feb 2001 21:28:23 +0100] rev 11028
moved to Product_Type_lemmas.ML
oheimb [Thu, 01 Feb 2001 20:56:21 +0100] rev 11027
added translations for bind_thm and val
oheimb [Thu, 01 Feb 2001 20:53:13 +0100] rev 11026
converted to Isar, simplifying recursion on class hierarchy
oheimb [Thu, 01 Feb 2001 20:51:48 +0100] rev 11025
converted to Isar therory, adding attributes complete_split and split_format
wenzelm [Thu, 01 Feb 2001 20:51:13 +0100] rev 11024
converted to new-style theories;
wenzelm [Thu, 01 Feb 2001 20:48:58 +0100] rev 11023
updated
wenzelm [Thu, 01 Feb 2001 20:45:54 +0100] rev 11022
ext_classrel: certify_class;
wenzelm [Thu, 01 Feb 2001 20:45:11 +0100] rev 11021
comment