| #
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
|