isabelle: Changelog

huffman [Fri, 18 May 2007 17:35:07 +0200] rev 23009

Prove existence of nth roots using Intermediate Value Theorem

huffman [Fri, 18 May 2007 16:13:07 +0200] rev 23008

avoid using real_mult_inverse_left; cleaned up

huffman [Fri, 18 May 2007 16:11:13 +0200] rev 23007

use mult_strict_mono instead of real_mult_less_mono

berghofe [Fri, 18 May 2007 11:12:03 +0200] rev 23006

Fixed bug in subst causing primrec functions returning functions to be rejected.

haftmann [Fri, 18 May 2007 09:16:57 +0200] rev 23005

dropped word_setup.ML

krauss [Thu, 17 May 2007 23:04:54 +0200] rev 23004

added files

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

isabelle