huffman [Fri, 11 May 2007 03:31:12 +0200] rev 22934
generalize setsum lemmas from semiring_0_cancel to semiring_0
wenzelm [Fri, 11 May 2007 01:07:10 +0200] rev 22933
tuned proofs;
wenzelm [Fri, 11 May 2007 00:43:46 +0200] rev 22932
bang_facts: warning;
wenzelm [Fri, 11 May 2007 00:43:45 +0200] rev 22931
tuned proofs;
haftmann [Thu, 10 May 2007 22:11:38 +0200] rev 22930
(class target)
haftmann [Thu, 10 May 2007 22:11:37 +0200] rev 22929
cleaned up
haftmann [Thu, 10 May 2007 22:11:36 +0200] rev 22928
beta/eta conversion after preprocessor
haftmann [Thu, 10 May 2007 22:11:35 +0200] rev 22927
fixed typo
wenzelm [Thu, 10 May 2007 18:10:32 +0200] rev 22926
more conversions;
tuned;
berghofe [Thu, 10 May 2007 15:51:59 +0200] rev 22925
Moved extraction_expand declaration of listall_def outside of definition.
berghofe [Thu, 10 May 2007 15:50:56 +0200] rev 22924
Adapted to new naming scheme for definitions.
berghofe [Thu, 10 May 2007 15:50:28 +0200] rev 22923
Changed name of raw definition.
berghofe [Thu, 10 May 2007 15:49:31 +0200] rev 22922
Name of ML function "not" is now qualified in order to avoid
clashes with names of constants introduced by the user.
haftmann [Thu, 10 May 2007 10:22:17 +0200] rev 22921
consts in consts_code Isar commands are now referred to by usual term syntax
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
wenzelm [Thu, 10 May 2007 00:39:56 +0200] rev 22910
moved conversions to structure Conv;
get_axiom_i;
wenzelm [Thu, 10 May 2007 00:39:55 +0200] rev 22909
added dest_fun/fun2/arg1;
removed dest_binop;
renamed cterm_(fo_)match to (fo_)match;
renamed cterm_incr_indexes to incr_indexes_cterm;
wenzelm [Thu, 10 May 2007 00:39:54 +0200] rev 22908
tuned argument_type_of;
wenzelm [Thu, 10 May 2007 00:39:53 +0200] rev 22907
added destructors from drule.ML;
added mk_binop;