isabelle: Changelog

krauss [Thu, 17 May 2007 23:03:47 +0200] rev 23003

updated

krauss [Thu, 17 May 2007 23:00:06 +0200] rev 23002

moved lemmas to Nat.thy

krauss [Thu, 17 May 2007 22:58:53 +0200] rev 23001

added induction principles for induction "backwards": P (Suc n) ==> P n

krauss [Thu, 17 May 2007 22:37:34 +0200] rev 23000

added pointer to new Unification theory

krauss [Thu, 17 May 2007 22:33:41 +0200] rev 22999

Added unification case study (using new function package)

huffman [Thu, 17 May 2007 21:51:32 +0200] rev 22998

avoid using redundant lemmas from RealDef.thy

haftmann [Thu, 17 May 2007 19:49:40 +0200] rev 22997

canonical prefixing of class constants

haftmann [Thu, 17 May 2007 19:49:21 +0200] rev 22996

dropped beta/eta normalization of defining equations

haftmann [Thu, 17 May 2007 19:49:20 +0200] rev 22995

refined pow function

haftmann [Thu, 17 May 2007 19:49:17 +0200] rev 22994

abstract size function in hologic.ML

isabelle