isabelle: Changelog

haftmann [Sat, 19 May 2007 11:33:20 +0200] rev 23016

added Executable_Real

haftmann [Sat, 19 May 2007 11:33:19 +0200] rev 23015

updated

nipkow [Sat, 19 May 2007 08:43:15 +0200] rev 23014

Had to replace "case 1/2" by "case base/step". No idea why.

nipkow [Sat, 19 May 2007 07:47:51 +0200] rev 23013

*** empty log message ***

huffman [Sat, 19 May 2007 04:52:24 +0200] rev 23012

remove dependence on Hilbert_Choice.thy

huffman [Sat, 19 May 2007 04:51:03 +0200] rev 23011

use THE instead of SOME

huffman [Fri, 18 May 2007 18:20:39 +0200] rev 23010

minimize imports

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

isabelle