huffman [Thu, 19 Feb 2009 12:26:32 -0800] rev 29995
add rule for minus 1 at type bit
huffman [Thu, 19 Feb 2009 12:03:31 -0800] rev 29994
add formalization of a type of integers mod 2 to Library
huffman [Thu, 19 Feb 2009 09:42:23 -0800] rev 29993
new theory of real inner product spaces
huffman [Thu, 19 Feb 2009 09:39:49 -0800] rev 29992
add Powerdomain_ex.thy
huffman [Thu, 19 Feb 2009 08:07:52 -0800] rev 29991
add more ordering lemmas
huffman [Thu, 19 Feb 2009 06:47:06 -0800] rev 29990
avoid using ab_semigroup_idem_mult locale for powerdomains
huffman [Thu, 19 Feb 2009 05:50:26 -0800] rev 29989
merged
huffman [Wed, 18 Feb 2009 20:53:58 -0800] rev 29988
add header
huffman [Wed, 18 Feb 2009 20:14:45 -0800] rev 29987
move Polynomial.thy to Library
huffman [Wed, 18 Feb 2009 19:51:39 -0800] rev 29986
move FrechetDeriv.thy to Library
huffman [Wed, 18 Feb 2009 19:32:26 -0800] rev 29985
split polynomial-related stuff from Deriv.thy into Library/Poly_Deriv.thy
kleing [Thu, 19 Feb 2009 23:55:10 +1100] rev 29984
half auto_solve default time out; increase manually in PG for large projects
(L4v/Verisoft large).
huffman [Wed, 18 Feb 2009 17:02:38 -0800] rev 29983
merged
huffman [Wed, 18 Feb 2009 17:02:00 -0800] rev 29982
finish converting Deriv.thy to new polynomial library
huffman [Wed, 18 Feb 2009 15:01:53 -0800] rev 29981
generalize int_dvd_cancel_factor simproc to idom class
huffman [Wed, 18 Feb 2009 14:17:04 -0800] rev 29980
composition of polynomials
huffman [Wed, 18 Feb 2009 12:24:06 -0800] rev 29979
add some lemmas, cleaned up
huffman [Wed, 18 Feb 2009 10:24:48 -0800] rev 29978
generalize le_imp_power_dvd and power_le_dvd; move from Divides to Power
huffman [Wed, 18 Feb 2009 09:47:58 -0800] rev 29977
move polynomial order stuff from Fundamental_Theorem_Algebra to Polynomial
huffman [Wed, 18 Feb 2009 09:08:04 -0800] rev 29976
merged
huffman [Wed, 18 Feb 2009 09:07:36 -0800] rev 29975
more subsection headings
huffman [Wed, 18 Feb 2009 07:24:13 -0800] rev 29974
speed up proof of exp_exists
haftmann [Wed, 18 Feb 2009 19:18:34 +0100] rev 29973
tuned
haftmann [Wed, 18 Feb 2009 19:18:33 +0100] rev 29972
sort instances wrt. to class hierarchy
haftmann [Wed, 18 Feb 2009 19:18:33 +0100] rev 29971
fixed signature
haftmann [Wed, 18 Feb 2009 19:18:32 +0100] rev 29970
tuned accessor name
haftmann [Wed, 18 Feb 2009 19:18:32 +0100] rev 29969
more precise improvement in instantiation user space type system
haftmann [Wed, 18 Feb 2009 19:18:31 +0100] rev 29968
do not drop arguments to 0, 1
haftmann [Wed, 18 Feb 2009 13:39:16 +0100] rev 29967
merged
haftmann [Wed, 18 Feb 2009 13:39:05 +0100] rev 29966
reverted to previous version of Finite_Set.thy
haftmann [Wed, 18 Feb 2009 11:31:05 +0100] rev 29965
merged
haftmann [Wed, 18 Feb 2009 08:23:45 +0100] rev 29964
merged
haftmann [Wed, 18 Feb 2009 08:23:12 +0100] rev 29963
first working version
haftmann [Wed, 18 Feb 2009 08:23:11 +0100] rev 29962
tuned comments, stripped ID, deleted superfluous code
haftmann [Wed, 18 Feb 2009 08:23:11 +0100] rev 29961
stripped ID
paulson [Wed, 18 Feb 2009 11:18:01 +0000] rev 29960
Syntactic support for products over set intervals
paulson [Wed, 18 Feb 2009 11:17:29 +0000] rev 29959
No idea what happened here!
paulson [Tue, 17 Feb 2009 10:03:58 +0000] rev 29958
Even and odd powers of -1
blanchet [Wed, 18 Feb 2009 10:26:48 +0100] rev 29957
merged
blanchet [Tue, 17 Feb 2009 14:01:54 +0100] rev 29956
Reintroduce set_interpreter for Collect and op :.
I removed them by accident when removing old code that dealt with the "set" type.
Incidentally, there is still some broken "set" code in Refute that should be fixed (see TODO in refute.ML).
blanchet [Mon, 16 Feb 2009 20:33:23 +0100] rev 29955
Added Nitpick tag to 'of_int_of_nat'.
This theorem leads to a more efficient encoding to Kodkod than the definition of 'of_int'.
huffman [Tue, 17 Feb 2009 20:45:23 -0800] rev 29954
add lemmas for exponentiation
haftmann [Tue, 17 Feb 2009 21:51:52 +0100] rev 29953
merged
haftmann [Tue, 17 Feb 2009 18:45:41 +0100] rev 29952
unified variable names in case expressions; no exponential fork in translation of case expressions
huffman [Tue, 17 Feb 2009 10:52:55 -0800] rev 29951
merged
huffman [Tue, 17 Feb 2009 07:13:29 -0800] rev 29950
remove redundant simp attributes for zdvd rules
huffman [Tue, 17 Feb 2009 06:59:33 -0800] rev 29949
lemmas abs_dvd_iff, dvd_abs_iff
nipkow [Tue, 17 Feb 2009 18:48:17 +0100] rev 29948
Cleaned up IntDiv and removed subsumed lemmas.
huffman [Mon, 16 Feb 2009 19:35:52 -0800] rev 29947
tune section headings; add square function
huffman [Mon, 16 Feb 2009 13:42:45 -0800] rev 29946
merged
huffman [Mon, 16 Feb 2009 13:42:15 -0800] rev 29945
rearrange subsections
huffman [Mon, 16 Feb 2009 13:14:36 -0800] rev 29944
remove instances num::semiring and num::linorder
huffman [Mon, 16 Feb 2009 13:08:21 -0800] rev 29943
datatype num = One | Dig0 num | Dig1 num
huffman [Mon, 16 Feb 2009 12:53:59 -0800] rev 29942
replace 1::num with One; remove monoid_mult instance
huffman [Sun, 15 Feb 2009 19:53:20 -0800] rev 29941
replace dec with double-and-decrement function
haftmann [Mon, 16 Feb 2009 19:11:55 +0100] rev 29940
more default simp rules for sgn
haftmann [Mon, 16 Feb 2009 19:11:35 +0100] rev 29939
re-generated
haftmann [Mon, 16 Feb 2009 19:11:16 +0100] rev 29938
clarified import
haftmann [Mon, 16 Feb 2009 19:11:16 +0100] rev 29937
faster preprocessor
haftmann [Mon, 16 Feb 2009 19:11:15 +0100] rev 29936
added pdivmod on int (for code generation)
haftmann [Mon, 16 Feb 2009 13:38:17 +0100] rev 29935
merged
haftmann [Mon, 16 Feb 2009 13:38:10 +0100] rev 29934
tuned texts
haftmann [Mon, 16 Feb 2009 13:38:09 +0100] rev 29933
dropped Id
haftmann [Mon, 16 Feb 2009 13:38:09 +0100] rev 29932
dropped clause_suc_preproc for generic code generator
haftmann [Mon, 16 Feb 2009 13:38:08 +0100] rev 29931
new primrec
berghofe [Mon, 16 Feb 2009 12:30:06 +0100] rev 29930
Adapted to encoding of sets as predicates.
kleing [Mon, 16 Feb 2009 20:45:15 +1100] rev 29929
enable auto-solve by default
blanchet [Mon, 16 Feb 2009 10:15:43 +0100] rev 29928
merged
blanchet [Mon, 16 Feb 2009 10:13:30 +0100] rev 29927
Added nitpick attribute, and fixed typo.
blanchet [Mon, 16 Feb 2009 10:11:20 +0100] rev 29926
Added myself to testing list.
nipkow [Sun, 15 Feb 2009 22:58:02 +0100] rev 29925
dvd and setprod lemmas
nipkow [Sun, 15 Feb 2009 16:25:39 +0100] rev 29924
merged
nipkow [Sun, 15 Feb 2009 16:25:16 +0100] rev 29923
added finite_set_choice
krauss [Sun, 15 Feb 2009 14:02:27 +0100] rev 29922
reject defined function in patterns with errmsg, e.g. f (f x) = x
nipkow [Sun, 15 Feb 2009 11:34:46 +0100] rev 29921
fixed document
nipkow [Sun, 15 Feb 2009 11:26:38 +0100] rev 29920
more finiteness
nipkow [Sun, 15 Feb 2009 07:54:46 +0100] rev 29919
merged
nipkow [Sun, 15 Feb 2009 07:54:16 +0100] rev 29918
more finiteness
nipkow [Sat, 14 Feb 2009 19:27:26 +0100] rev 29917
merged
nipkow [Sat, 14 Feb 2009 19:27:15 +0100] rev 29916
more finiteness
huffman [Sat, 14 Feb 2009 19:01:31 -0800] rev 29915
generalize lemma fps_square_eq_iff, move to Ring_and_Field
huffman [Sat, 14 Feb 2009 16:51:18 -0800] rev 29914
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman [Sat, 14 Feb 2009 15:30:26 -0800] rev 29913
add mult_delta lemmas; simplify some proofs
huffman [Sat, 14 Feb 2009 11:32:35 -0800] rev 29912
fix spelling
huffman [Sat, 14 Feb 2009 11:11:30 -0800] rev 29911
declare fps_nth as a typedef morphism; clean up instance proofs
huffman [Sat, 14 Feb 2009 11:10:35 -0800] rev 29910
add lemma surj_from_nat
huffman [Sat, 14 Feb 2009 06:53:28 -0800] rev 29909
fix document generation
huffman [Sat, 14 Feb 2009 01:24:01 -0800] rev 29908
merged
huffman [Sat, 14 Feb 2009 01:23:38 -0800] rev 29907
fix document generation
huffman [Fri, 13 Feb 2009 14:45:10 -0800] rev 29906
section -> subsection
huffman [Fri, 13 Feb 2009 14:41:54 -0800] rev 29905
add instance for cancel_comm_monoid_add
huffman [Fri, 13 Feb 2009 14:12:00 -0800] rev 29904
add class cancel_comm_monoid_add
nipkow [Sat, 14 Feb 2009 08:45:16 +0100] rev 29903
more finiteness changes
nipkow [Fri, 13 Feb 2009 23:55:24 +0100] rev 29902
merged
nipkow [Fri, 13 Feb 2009 23:55:04 +0100] rev 29901
finiteness lemmas
huffman [Fri, 13 Feb 2009 12:07:03 -0800] rev 29900
merged
huffman [Fri, 13 Feb 2009 12:06:09 -0800] rev 29899
unset execute bit
berghofe [Fri, 13 Feb 2009 16:47:08 +0100] rev 29898
Tuned datatype antiquotation.
haftmann [Fri, 13 Feb 2009 13:28:14 +0100] rev 29897
made SMLNJ happy
kleing [Fri, 13 Feb 2009 21:14:30 +1100] rev 29896
typo
kleing [Fri, 13 Feb 2009 16:00:45 +1100] rev 29895
find_consts: display the search criteria. (by Timothy Bourke)
kleing [Fri, 13 Feb 2009 14:57:25 +1100] rev 29894
find_consts: documentation. (by Timothy Bourke)
kleing [Fri, 13 Feb 2009 11:49:02 +1100] rev 29893
FindTheorems solves: update documentation (by Timothy Bourke)
haftmann [Fri, 13 Feb 2009 10:41:56 +0100] rev 29892
fixed codegen tool
haftmann [Fri, 13 Feb 2009 10:30:26 +0100] rev 29891
merged
haftmann [Fri, 13 Feb 2009 10:30:13 +0100] rev 29890
fixed codegen tool
nipkow [Fri, 13 Feb 2009 09:56:24 +0100] rev 29889
merged
nipkow [Fri, 13 Feb 2009 09:54:47 +0100] rev 29888
Moved Nat_Int_Bij into Library
haftmann [Fri, 13 Feb 2009 08:59:06 +0100] rev 29887
removed Reflection session
huffman [Thu, 12 Feb 2009 21:24:14 -0800] rev 29886
add lemma add_nonneg_eq_0_iff
huffman [Thu, 12 Feb 2009 20:36:41 -0800] rev 29885
add lemmas about sgn
kleing [Fri, 13 Feb 2009 08:00:46 +1100] rev 29884
added ML file for the find_consts command
kleing [Fri, 13 Feb 2009 07:59:30 +1100] rev 29883
added find_consts to NEWS and CONTRIBUTORS
kleing [Fri, 13 Feb 2009 07:53:38 +1100] rev 29882
New command find_consts searching for constants by type (by Timothy Bourke).
huffman [Thu, 12 Feb 2009 12:35:45 -0800] rev 29881
fix document generation
huffman [Thu, 12 Feb 2009 11:04:22 -0800] rev 29880
move countability proof from Rational to Countable; add instance rat :: countable
nipkow [Thu, 12 Feb 2009 18:14:43 +0100] rev 29879
Moved FTA into Lib and cleaned it up a little.
huffman [Wed, 11 Feb 2009 11:22:42 -0800] rev 29878
ordered_idom instance for polynomials
krauss [Wed, 11 Feb 2009 19:31:20 +0100] rev 29877
Export tactic interface for sizechange method
haftmann [Wed, 11 Feb 2009 15:05:40 +0100] rev 29876
merged