#
c5b95729 |
|
08-Mar-2020 |
haftmann <none@none> |
more frugal simp rules for bit operations; more pervasive use of bit selector --HG-- extra : rebase_source : 09f56fd30f4ab8ae84811041575772264eb330b3
|
#
4330682e |
|
11-Feb-2020 |
haftmann <none@none> |
tuned proof --HG-- extra : rebase_source : cb8a9a47d749a11c11cdcb0c08c5614134b47e23
|
#
08b2d734 |
|
09-Feb-2020 |
haftmann <none@none> |
easy abstraction over pointwise bit operations
|
#
a1a97176 |
|
09-Feb-2020 |
haftmann <none@none> |
rule concerning bit (push_bit ...)
|
#
32c7b8a2 |
|
09-Feb-2020 |
haftmann <none@none> |
more lemmas
|
#
7dbe6a33 |
|
03-Feb-2020 |
haftmann <none@none> |
more theorems --HG-- extra : rebase_source : 31d1d11efc3dadafd324be532d0cc208392e6c53
|
#
fb14e7d9 |
|
01-Feb-2020 |
haftmann <none@none> |
more specific class assumptions
|
#
12779091 |
|
01-Feb-2020 |
haftmann <none@none> |
more theorems
|
#
41860e03 |
|
26-Jan-2020 |
haftmann <none@none> |
more theorems --HG-- extra : rebase_source : e3c03fae6f0b037ea348b764e1ca0580c3370d43
|
#
f3b05a1f |
|
02-Dec-2019 |
haftmann <none@none> |
tuned material --HG-- extra : rebase_source : 28017ca9e3c54a758db0e8c3ac45e1c2b31b6f65
|
#
57769df1 |
|
01-Dec-2019 |
haftmann <none@none> |
characterization of singleton bit operation
|
#
2dfccec5 |
|
27-Nov-2019 |
haftmann <none@none> |
bit accessor and fundamental properties --HG-- extra : rebase_source : e5f56820c0cef29329c52101f9468736c9545132
|
#
676e878e |
|
23-Nov-2019 |
haftmann <none@none> |
tuned theory structure --HG-- extra : rebase_source : 5c815fe78ad41f3c4359e94e37f533cb90010da0
|
#
936f4b2b |
|
17-Nov-2019 |
haftmann <none@none> |
strengthened type class for bit operations
|
#
3b6cecbe |
|
09-Nov-2019 |
haftmann <none@none> |
bit shifts as class operations
|
#
142925a6 |
|
31-Oct-2019 |
haftmann <none@none> |
more lemmas --HG-- extra : rebase_source : f39e5acccf1b128cb41ebec1bcb75b0b34efb061
|
#
a6ddae93 |
|
19-Oct-2019 |
haftmann <none@none> |
more lemmas
|
#
e6ca3b44 |
|
17-Jul-2019 |
paulson <lp15@cam.ac.uk> |
a few new lemmas and a bit of tidying
|
#
d3b799f6 |
|
16-Jun-2019 |
haftmann <none@none> |
even more appropriate fact name --HG-- extra : rebase_source : c84aa5a47240766b900dbcb7659c7f68e6eb7a35
|
#
993b8b1c |
|
14-Jun-2019 |
haftmann <none@none> |
generalized type classes for parity to cover word types also, which contain zero divisors
|
#
6ee2be1e |
|
14-Jun-2019 |
haftmann <none@none> |
slightly more specialized name for type class
|
#
a78ecebc |
|
14-Jun-2019 |
haftmann <none@none> |
dropped weaker legacy alias
|
#
c71aaa04 |
|
14-Jun-2019 |
haftmann <none@none> |
slightly more stringent ordering of theorems
|
#
fe03936a |
|
01-May-2019 |
haftmann <none@none> |
more lemmas --HG-- extra : rebase_source : 3e2ac977160873ea4b0f5fb90c505d1a2c674b91
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
05936fb0 |
|
23-Dec-2018 |
haftmann <none@none> |
more rules
|
#
8dddbfd5 |
|
27-Oct-2018 |
nipkow <none@none> |
moved lemmas
|
#
603dda4f |
|
06-Jun-2018 |
wenzelm <none@none> |
proper white space;
|
#
8280abe0 |
|
12-May-2018 |
haftmann <none@none> |
removed some non-essential rules
|
#
3a4a7136 |
|
24-Apr-2018 |
haftmann <none@none> |
proper datatype for 8-bit characters
|
#
79b69ae3 |
|
20-Apr-2018 |
haftmann <none@none> |
algebraic embeddings for bit operations
|
#
419f46a8 |
|
15-Apr-2018 |
haftmann <none@none> |
explicit simp rules for computing abstract bit operations
|
#
53f44535 |
|
05-Apr-2018 |
haftmann <none@none> |
even more on bit operations
|
#
a833d6ec |
|
04-Apr-2018 |
haftmann <none@none> |
more bit operation conversions
|
#
1a5906f0 |
|
21-Mar-2018 |
haftmann <none@none> |
tuned proof
|
#
0893d241 |
|
21-Mar-2018 |
haftmann <none@none> |
prefer convention to place operation name before type name
|
#
323bf0b5 |
|
20-Mar-2018 |
haftmann <none@none> |
more lemmas
|
#
bef5ff04 |
|
20-Mar-2018 |
haftmann <none@none> |
generalized
|
#
89bc0179 |
|
12-Mar-2018 |
haftmann <none@none> |
eliminiated superfluous class semiring_bits
|
#
0b6326bb |
|
10-Mar-2018 |
haftmann <none@none> |
abstract algebraic bit operations --HG-- extra : rebase_source : 10402190e8858b0ea47b7ac7f91671a9935921ae
|
#
97f38ec1 |
|
08-Jan-2018 |
paulson <lp15@cam.ac.uk> |
moved in some material from Euler-MacLaurin
|
#
ca3200e3 |
|
23-Nov-2017 |
haftmann <none@none> |
new simp rule
|
#
85b3e948 |
|
11-Nov-2017 |
haftmann <none@none> |
dedicated definition for coprimality --HG-- extra : rebase_source : 891168c98ce62efae6b7e72c7d3365fea12b33ae
|
#
0cca2e53 |
|
09-Oct-2017 |
haftmann <none@none> |
canonical multiplicative euclidean size --HG-- extra : rebase_source : fad957bbd86aef396df70a1acd8bd096a0a3c82b
|
#
2c72473b |
|
09-Oct-2017 |
haftmann <none@none> |
clarified parity --HG-- extra : rebase_source : 7e46e7dfc0f09316c589babeb5a372aeff091071
|
#
f740f805 |
|
08-Oct-2017 |
haftmann <none@none> |
more fundamental definition of div and mod on int --HG-- extra : rebase_source : 95b72d036b88e199c61235ea5833a905f5632800
|
#
de79d13d |
|
08-Oct-2017 |
haftmann <none@none> |
one uniform type class for parity structures --HG-- extra : rebase_source : edf12af006cee8d114754f4a1916094166004337
|
#
b01640ea |
|
08-Oct-2017 |
haftmann <none@none> |
elementary definition of division on natural numbers --HG-- extra : rebase_source : 23767fa1baf28db39b18de60e52d4d7f852e48dd
|
#
f2ca1190 |
|
26-Aug-2017 |
bulwahn <none@none> |
another fact on (- 1) ^ _ --HG-- extra : rebase_source : 4b559c07dffee156c9a1e8ad6847a02880960ca5
|
#
cc698c8d |
|
04-Jan-2017 |
haftmann <none@none> |
moved euclidean ring to HOL --HG-- extra : rebase_source : f98dc2e61ffb3cbd04e533f3c0cffa028129e4a2
|
#
1667fe95 |
|
10-Aug-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
#
8175ce0f |
|
12-Mar-2016 |
haftmann <none@none> |
model characters directly as range 0..255 * * * operate on syntax terms rather than asts
|
#
5ad25152 |
|
05-Jan-2016 |
hoelzl <none@none> |
add the proof of the central limit theorem --HG-- extra : rebase_source : 493d99e28392771c51f4102a11b90533880e289f extra : amend_source : 3fb7b7c607104e57a2c3ba7f733dd570eb42fa3b
|
#
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
dd88f1ec |
|
02-Nov-2015 |
eberlm <none@none> |
Rounding function, uniform limits, cotangent, binomial identities
|
#
6ee65982 |
|
06-Aug-2015 |
haftmann <none@none> |
slight cleanup of lemmas --HG-- extra : rebase_source : 17dbf1b3c59a40c2a2ac93ab58d3e6371773af6c
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
456b0fa3 |
|
23-Jun-2015 |
paulson <lp15@cam.ac.uk> |
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
|
#
975b8889 |
|
01-Jun-2015 |
haftmann <none@none> |
correct sort constraints for abbreviations in type classes * * * yet another bunch of corrections
|
#
8c67c983 |
|
23-Mar-2015 |
haftmann <none@none> |
distributivity of partial minus establishes desired properties of dvd in semirings --HG-- extra : rebase_source : 99dad957de0410b3a1ca21ff1f8723495b31194f
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
338f82d5 |
|
26-Oct-2014 |
haftmann <none@none> |
eliminated redundancies; more simp rules --HG-- extra : rebase_source : d2f3410108e72d87e8aafe6b8721e88136c940cf
|
#
b3f0459b |
|
23-Oct-2014 |
haftmann <none@none> |
even further downshift of theory Parity in the hierarchy --HG-- extra : rebase_source : d3582456671ff992f3d453a0def98065cde7db5a
|
#
edd58f80 |
|
23-Oct-2014 |
haftmann <none@none> |
further downshift of theory Parity in the hierarchy --HG-- extra : rebase_source : e7215b85854d21232ca65e2ca813246deda9624b
|
#
9dcbeb6a |
|
23-Oct-2014 |
haftmann <none@none> |
slight generalization and unification of simp rules for algebraic procedures
|
#
06e59c9f |
|
23-Oct-2014 |
haftmann <none@none> |
downshift of theory Parity in the hierarchy
|
#
d6ff9496 |
|
23-Oct-2014 |
haftmann <none@none> |
parity induction over natural numbers
|
#
8153684f |
|
21-Oct-2014 |
haftmann <none@none> |
turn even into an abbreviation
|
#
37727d41 |
|
20-Oct-2014 |
wenzelm <none@none> |
repared document;
|
#
4d0a49b6 |
|
19-Oct-2014 |
haftmann <none@none> |
more standard declaration for presburger
|
#
830e17f5 |
|
19-Oct-2014 |
haftmann <none@none> |
augmented and tuned facts on even/odd and division
|
#
3c2ea5d6 |
|
19-Oct-2014 |
haftmann <none@none> |
prefer generic elimination rules for even/odd over specialized unfold rules for nat
|
#
8ba1da82 |
|
16-Oct-2014 |
haftmann <none@none> |
tuned
|
#
6354ed8d |
|
16-Oct-2014 |
haftmann <none@none> |
standard elimination rule for even
|
#
f4d80892 |
|
16-Oct-2014 |
haftmann <none@none> |
tuned facts on even and power
|
#
84780740 |
|
16-Oct-2014 |
haftmann <none@none> |
restructured
|
#
de968c7b |
|
16-Oct-2014 |
haftmann <none@none> |
even more cleanup
|
#
caf0f7d9 |
|
14-Oct-2014 |
haftmann <none@none> |
legacy cleanup --HG-- extra : rebase_source : b783230cb4dbeaff039ed70035a3a54de2f94da0
|
#
d8b66e19 |
|
14-Oct-2014 |
haftmann <none@none> |
more algebraic deductions for facts on even/odd --HG-- extra : rebase_source : f2cf55287993cdf31639e96d96c2404b53fd7263
|
#
b528455b |
|
14-Oct-2014 |
haftmann <none@none> |
more algebraic deductions for facts on even/odd --HG-- extra : rebase_source : 45413979a6b0613a898e69d6b877206bc380e581
|
#
c40742cc |
|
14-Oct-2014 |
haftmann <none@none> |
purely algebraic characterization of even and odd --HG-- extra : rebase_source : 0fe26a67bd01567912f5de98b2c1053ee5175683
|
#
49fd3272 |
|
09-Oct-2014 |
haftmann <none@none> |
more foundational definition for predicate even --HG-- extra : rebase_source : 2ab438f007b79510c2c1ad8092315e3043786b93
|
#
138816de |
|
19-Nov-2013 |
haftmann <none@none> |
eliminiated neg_numeral in favour of - (numeral _)
|
#
f1147be0 |
|
31-Oct-2013 |
haftmann <none@none> |
purely algebraic foundation for even/odd --HG-- extra : rebase_source : 084e35534919330b363f3c995c75159de32dfa54
|
#
7352f49b |
|
31-Oct-2013 |
haftmann <none@none> |
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas; tuned presburger --HG-- extra : rebase_source : 30fe190a27dae1b09024f4fdd70ee005a33e99ba
|
#
ad7f9be9 |
|
30-Mar-2012 |
huffman <none@none> |
remove redundant simp rule
|
#
ba9336b3 |
|
30-Mar-2012 |
huffman <none@none> |
add simp rules for eve/odd on numerals
|
#
0a8fe6fe |
|
27-Mar-2012 |
huffman <none@none> |
remove redundant lemma
|
#
8bb6233a |
|
25-Mar-2012 |
huffman <none@none> |
merged fork with new numeral representation (see NEWS)
|
#
a495a026 |
|
20-Nov-2011 |
wenzelm <none@none> |
eliminated obsolete "standard";
|
#
6b0b29ec |
|
13-Mar-2011 |
wenzelm <none@none> |
tuned headers;
|
#
105cfb65 |
|
11-May-2010 |
huffman <none@none> |
fix duplicate simp rule warning
|
#
26cd7fb3 |
|
06-May-2010 |
haftmann <none@none> |
tuned proof
|
#
297293d7 |
|
08-Mar-2010 |
haftmann <none@none> |
transfer: avoid camel case
|
#
7417b1b7 |
|
06-Mar-2010 |
huffman <none@none> |
generalize some lemmas from class linordered_ring_strict to linordered_ring
|
#
aaaa7964 |
|
18-Feb-2010 |
huffman <none@none> |
get rid of many duplicate simp rule warnings
|
#
d03259c6 |
|
08-Feb-2010 |
haftmann <none@none> |
dropped accidental duplication of "lin" prefix from cs. 108662d50512
|
#
5d17693c |
|
05-Feb-2010 |
haftmann <none@none> |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
#
90daa6da |
|
30-Oct-2009 |
haftmann <none@none> |
moved some div/mod lemmas to theory Divides
|
#
7d4dc9b8 |
|
29-Oct-2009 |
haftmann <none@none> |
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
|
#
742c99c4 |
|
19-Jun-2009 |
nipkow <none@none> |
fixed thm name
|
#
869ba495 |
|
14-May-2009 |
nipkow <none@none> |
Cleaned up Parity a little
|
#
baadc210 |
|
28-Apr-2009 |
haftmann <none@none> |
stripped class recpower further
|
#
262e6aa4 |
|
27-Mar-2009 |
haftmann <none@none> |
normalized imports
|
#
121e82fb |
|
04-Mar-2009 |
blanchet <none@none> |
Merge.
|
#
6b788c26 |
|
22-Feb-2009 |
nipkow <none@none> |
added lemmas
|
#
92153b8c |
|
05-Feb-2009 |
hoelzl <none@none> |
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
|
#
9c7f19c4 |
|
28-Jan-2009 |
haftmann <none@none> |
Plain, Main form meeting points in import hierarchy
|
#
c49b40c1 |
|
21-Jan-2009 |
haftmann <none@none> |
no base sort in class import
|
#
f21befe1 |
|
03-Dec-2008 |
haftmann <none@none> |
made repository layout more coherent with logical distribution structure; stripped some $Id$s --HG-- rename : src/HOL/Library/Code_Message.thy => src/HOL/Code_Message.thy rename : src/HOL/Complex/Complex.thy => src/HOL/Complex.thy rename : src/HOL/Complex/Complex_Main.thy => src/HOL/Complex_Main.thy rename : src/HOL/Real/ContNotDenum.thy => src/HOL/ContNotDenum.thy rename : src/HOL/Hyperreal/Deriv.thy => src/HOL/Deriv.thy rename : src/HOL/Hyperreal/Fact.thy => src/HOL/Fact.thy rename : src/HOL/Hyperreal/FrechetDeriv.thy => src/HOL/FrechetDeriv.thy rename : src/HOL/Library/GCD.thy => src/HOL/GCD.thy rename : src/HOL/Hyperreal/Integration.thy => src/HOL/Integration.thy rename : src/HOL/Real/Float.thy => src/HOL/Library/Float.thy rename : src/HOL/Hyperreal/Lim.thy => src/HOL/Lim.thy rename : src/HOL/Hyperreal/Ln.thy => src/HOL/Ln.thy rename : src/HOL/Hyperreal/Log.thy => src/HOL/Log.thy rename : src/HOL/Real/Lubs.thy => src/HOL/Lubs.thy rename : src/HOL/Hyperreal/MacLaurin.thy => src/HOL/MacLaurin.thy rename : src/HOL/Hyperreal/NthRoot.thy => src/HOL/NthRoot.thy rename : src/HOL/Library/Order_Relation.thy => src/HOL/Order_Relation.thy rename : src/HOL/Real/PReal.thy => src/HOL/PReal.thy rename : src/HOL/Library/Parity.thy => src/HOL/Parity.thy rename : src/HOL/Real/RComplete.thy => src/HOL/RComplete.thy rename : src/HOL/Real/Rational.thy => src/HOL/Rational.thy rename : src/HOL/Real/Real.thy => src/HOL/Real.thy rename : src/HOL/Real/RealDef.thy => src/HOL/RealDef.thy rename : src/HOL/Real/RealPow.thy => src/HOL/RealPow.thy rename : src/HOL/Hyperreal/Series.thy => src/HOL/Series.thy rename : src/HOL/Hyperreal/Taylor.thy => src/HOL/Taylor.thy rename : src/HOL/arith_data.ML => src/HOL/Tools/arith_data.ML rename : src/HOL/Real/float_arith.ML => src/HOL/Tools/float_arith.ML rename : src/HOL/Real/float_syntax.ML => src/HOL/Tools/float_syntax.ML rename : src/HOL/hologic.ML => src/HOL/Tools/hologic.ML rename : src/HOL/int_arith1.ML => src/HOL/Tools/int_arith.ML rename : src/HOL/int_factor_simprocs.ML => src/HOL/Tools/int_factor_simprocs.ML rename : src/HOL/nat_simprocs.ML => src/HOL/Tools/nat_simprocs.ML rename : src/HOL/Real/rat_arith.ML => src/HOL/Tools/rat_arith.ML rename : src/HOL/Real/real_arith.ML => src/HOL/Tools/real_arith.ML rename : src/HOL/simpdata.ML => src/HOL/Tools/simpdata.ML rename : src/HOL/Hyperreal/Transcendental.thy => src/HOL/Transcendental.thy rename : src/HOL/Library/RType.thy => src/HOL/Typerep.thy rename : src/HOL/Library/Univ_Poly.thy => src/HOL/Univ_Poly.thy rename : src/HOL/Complex/ex/Arithmetic_Series_Complex.thy => src/HOL/ex/Arithmetic_Series_Complex.thy rename : src/HOL/Complex/ex/BigO_Complex.thy => src/HOL/ex/BigO_Complex.thy rename : src/HOL/Complex/ex/HarmonicSeries.thy => src/HOL/ex/HarmonicSeries.thy rename : src/HOL/Complex/ex/MIR.thy => src/HOL/ex/MIR.thy rename : src/HOL/Complex/ex/ReflectedFerrack.thy => src/HOL/ex/ReflectedFerrack.thy rename : src/HOL/Complex/ex/Sqrt.thy => src/HOL/ex/Sqrt.thy rename : src/HOL/Complex/ex/Sqrt_Script.thy => src/HOL/ex/Sqrt_Script.thy rename : src/HOL/Complex/ex/linrtac.ML => src/HOL/ex/linrtac.ML rename : src/HOL/Complex/ex/mirtac.ML => src/HOL/ex/mirtac.ML rename : src/Pure/Tools/quickcheck.ML => src/Tools/quickcheck.ML rename : src/Pure/Tools/value.ML => src/Tools/value.ML
|