Mon, 14 May 2007 12:52:56 +0200 haftmann reorganized float arithmetic
Mon, 14 May 2007 12:52:54 +0200 haftmann fixed IntInf ambiguity
Mon, 14 May 2007 09:33:18 +0200 huffman remove redundant lemmas
Mon, 14 May 2007 09:27:24 +0200 huffman remove redundant lemmas
Mon, 14 May 2007 09:16:47 +0200 huffman remove redundant lemmas
Mon, 14 May 2007 09:11:30 +0200 huffman remove redundant lemmas
Mon, 14 May 2007 08:15:13 +0200 huffman cleaned up
Mon, 14 May 2007 08:12:38 +0200 huffman tuned
Sun, 13 May 2007 20:05:42 +0200 huffman define roots of negative reals so that many lemmas no longer require side conditions; simplification solves more goals than previously
Sun, 13 May 2007 19:15:36 +0200 huffman add lemma power_eq_imp_eq_base
Sun, 13 May 2007 18:16:49 +0200 haftmann added module int
Sun, 13 May 2007 18:15:30 +0200 haftmann dropped legacy
Sun, 13 May 2007 18:15:28 +0200 haftmann removed module rat.ML
Sun, 13 May 2007 18:15:26 +0200 haftmann whitespace tuned
Sun, 13 May 2007 18:15:25 +0200 haftmann tuned
Sun, 13 May 2007 18:15:24 +0200 haftmann fixed omission
Sun, 13 May 2007 18:15:23 +0200 haftmann tuned setup
Sun, 13 May 2007 18:15:22 +0200 haftmann refined module rat
Sun, 13 May 2007 18:15:21 +0200 haftmann added modules rat.ML and int.ML
Sun, 13 May 2007 09:23:27 +0200 nipkow Removed junk
Sun, 13 May 2007 07:11:21 +0200 nipkow Got rid of listsp
Sun, 13 May 2007 04:38:24 +0200 huffman removed redundant lemmas
Sat, 12 May 2007 18:16:30 +0200 huffman add lemma additive.setsum
Fri, 11 May 2007 20:47:30 +0200 nipkow *** empty log message ***
Fri, 11 May 2007 20:07:00 +0200 nipkow *** empty log message ***
Fri, 11 May 2007 18:49:15 +0200 wenzelm proper type for fun/arg_cong_rule;
Fri, 11 May 2007 18:47:08 +0200 wenzelm added fun/arg_cong_rule;
Fri, 11 May 2007 18:46:50 +0200 wenzelm unified names: foo_conv;
Fri, 11 May 2007 17:54:36 +0200 wenzelm tuned;
Fri, 11 May 2007 15:37:42 +0200 krauss added fun flip f x y = f y x
Fri, 11 May 2007 03:31:12 +0200 huffman generalize setsum lemmas from semiring_0_cancel to semiring_0
Fri, 11 May 2007 01:07:10 +0200 wenzelm tuned proofs;
Fri, 11 May 2007 00:43:46 +0200 wenzelm bang_facts: warning;
Fri, 11 May 2007 00:43:45 +0200 wenzelm tuned proofs;
Thu, 10 May 2007 22:11:38 +0200 haftmann (class target)
Thu, 10 May 2007 22:11:37 +0200 haftmann cleaned up
Thu, 10 May 2007 22:11:36 +0200 haftmann beta/eta conversion after preprocessor
Thu, 10 May 2007 22:11:35 +0200 haftmann fixed typo
Thu, 10 May 2007 18:10:32 +0200 wenzelm more conversions;
Thu, 10 May 2007 15:51:59 +0200 berghofe Moved extraction_expand declaration of listall_def outside of definition.
Thu, 10 May 2007 15:50:56 +0200 berghofe Adapted to new naming scheme for definitions.
Thu, 10 May 2007 15:50:28 +0200 berghofe Changed name of raw definition.
Thu, 10 May 2007 15:49:31 +0200 berghofe Name of ML function "not" is now qualified in order to avoid
Thu, 10 May 2007 10:22:17 +0200 haftmann consts in consts_code Isar commands are now referred to by usual term syntax
Thu, 10 May 2007 10:21:50 +0200 haftmann size [nat] is identity
Thu, 10 May 2007 10:21:48 +0200 haftmann explicit import of Datatype.thy due to hook bootstrap problem
Thu, 10 May 2007 10:21:47 +0200 haftmann localized Sup/Inf
Thu, 10 May 2007 10:21:46 +0200 haftmann localized Min/Max
Thu, 10 May 2007 10:21:44 +0200 haftmann tuned
Thu, 10 May 2007 04:06:56 +0200 huffman fix proofs
Thu, 10 May 2007 03:11:03 +0200 huffman remove redundant lemmas
Thu, 10 May 2007 03:07:26 +0200 huffman lemmas iszero_(h)complex_number_of are no longer needed
Thu, 10 May 2007 03:00:15 +0200 huffman instance real_algebra_1 < ring_char_0
Thu, 10 May 2007 02:51:53 +0200 huffman new axclass ring_char_0 for rings with characteristic 0, used for of_int_eq_iff and related lemmas
Thu, 10 May 2007 00:39:56 +0200 wenzelm moved conversions to structure Conv;
Thu, 10 May 2007 00:39:55 +0200 wenzelm added dest_fun/fun2/arg1;
Thu, 10 May 2007 00:39:54 +0200 wenzelm tuned argument_type_of;
Thu, 10 May 2007 00:39:53 +0200 wenzelm added destructors from drule.ML;
Thu, 10 May 2007 00:39:52 +0200 wenzelm moved some operations to more_thm.ML and conv.ML;
Thu, 10 May 2007 00:39:51 +0200 wenzelm Conversions: primitive equality reasoning (from drule.ML);
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip