isabelle: Changelog

haftmann [Thu, 10 May 2007 10:21:50 +0200] rev 22920

size [nat] is identity

haftmann [Thu, 10 May 2007 10:21:48 +0200] rev 22919

explicit import of Datatype.thy due to hook bootstrap problem

haftmann [Thu, 10 May 2007 10:21:47 +0200] rev 22918

localized Sup/Inf

haftmann [Thu, 10 May 2007 10:21:46 +0200] rev 22917

localized Min/Max

haftmann [Thu, 10 May 2007 10:21:44 +0200] rev 22916

tuned

huffman [Thu, 10 May 2007 04:06:56 +0200] rev 22915

fix proofs

huffman [Thu, 10 May 2007 03:11:03 +0200] rev 22914

remove redundant lemmas

huffman [Thu, 10 May 2007 03:07:26 +0200] rev 22913

lemmas iszero_(h)complex_number_of are no longer needed

huffman [Thu, 10 May 2007 03:00:15 +0200] rev 22912

instance real_algebra_1 < ring_char_0

huffman [Thu, 10 May 2007 02:51:53 +0200] rev 22911

new axclass ring_char_0 for rings with characteristic 0, used for of_int_eq_iff and related lemmas

isabelle