| #
6985f7d6 |
|
15-Jul-2018 |
Manuel Eberl <eberlm@in.tum.de> |
Added Real_Asymp package
|
| #
e1afdaa2 |
|
29-Jun-2018 |
wenzelm <none@none> |
tuned;
|
| #
b5651d18 |
|
29-Jun-2018 |
wenzelm <none@none> |
misc tuning and updates for release;
|
| #
d409cc61 |
|
29-Jun-2018 |
Wenda Li <wl302@cam.ac.uk> |
NEWS and CONTRIBUTORS
|
| #
1394cb87 |
|
28-Jun-2018 |
paulson <lp15@cam.ac.uk> |
Incorporating new/strengthened proofs from Library and AFP entries
|
| #
5c6f3ded |
|
27-Jun-2018 |
immler <none@none> |
example for Types_To_Sets: transfer from type-based linear algebra to subspaces
|
| #
0ebac218 |
|
18-Jun-2018 |
paulson <lp15@cam.ac.uk> |
corrections to markup
|
| #
78a54074 |
|
06-Jun-2018 |
wenzelm <none@none> |
updated for release;
tuned;
|
| #
24d56e0a |
|
18-May-2018 |
Manuel Eberl <eberlm@in.tum.de> |
Moved Landau_Symbols from the AFP to HOL-Library
--HG--
extra : rebase_source : 118ac657be82d7b9b2d3e14ff4e59f8b1c3b7b5c
|
| #
66083c13 |
|
16-May-2018 |
Andreas Lochbihler <none@none> |
NEWS and CONTRIBUTORS for 8b50f29a1992
|
| #
e04b7748 |
|
02-May-2018 |
immler <none@none> |
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
--HG--
rename : src/HOL/Library/FuncSet.thy => src/HOL/FuncSet.thy
|
| #
3a4a7136 |
|
24-Apr-2018 |
haftmann <none@none> |
proper datatype for 8-bit characters
|
| #
647b26c4 |
|
24-Apr-2018 |
haftmann <none@none> |
corrected nonsense
|
| #
88ea89c5 |
|
23-Mar-2018 |
haftmann <none@none> |
NEWS and CONTRIBUTORS
|
| #
39be15af |
|
12-Mar-2018 |
Manuel Eberl <eberlm@in.tum.de> |
Removed stray 'sledgehammer' invocation
|
| #
79b49c68 |
|
19-Jan-2018 |
nipkow <none@none> |
added lemma
|
| #
57a3edcb |
|
25-Dec-2017 |
haftmann <none@none> |
spelling
--HG--
extra : rebase_source : 6f25679c26ccff208c7faa86656ba44ca93dd2b8
|
| #
516a26c4 |
|
18-Dec-2017 |
traytel <none@none> |
a conditional paramitrecity prover
|
| #
f198f5f7 |
|
22-Oct-2017 |
nipkow <none@none> |
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
|
| #
a020c163 |
|
08-Sep-2017 |
wenzelm <none@none> |
back to post-release mode -- after fork point;
|
| #
c2aaa30e |
|
08-Sep-2017 |
wenzelm <none@none> |
tuned;
|
| #
e9b50e6b |
|
08-Sep-2017 |
paulson <lp15@cam.ac.uk> |
Lawrence Paulson's contributions
|
| #
56949984 |
|
08-Sep-2017 |
blanchet <none@none> |
listed contribution
|
| #
d644fa06 |
|
30-Aug-2017 |
Andreas Lochbihler <none@none> |
add type of unordered pairs
|
| #
a81834f3 |
|
22-Aug-2017 |
wenzelm <none@none> |
tuned;
|
| #
4756006d |
|
21-Aug-2017 |
Manuel Eberl <eberlm@in.tum.de> |
HOL-Analysis: Convergent FPS and infinite sums
--HG--
extra : rebase_source : 13cc70726e381a14afef3a3ace871ff02dfa8ba8
extra : amend_source : 24996647b80e5b6c0f6b19469f245f6b785df3a0
|
| #
599bcfe3 |
|
21-Aug-2017 |
wenzelm <none@none> |
misc updates for release;
|
| #
3b2aa882 |
|
20-Mar-2017 |
ballarin <none@none> |
Corrected affiliation.
|
| #
5df98fce |
|
02-Mar-2017 |
ballarin <none@none> |
Knaster-Tarski fixed point theorem and Galois Connections.
|
| #
ef73534c |
|
22-Feb-2017 |
haftmann <none@none> |
more precise NEWS and CONTRIBUTORS
|
| #
84d89437 |
|
22-Feb-2017 |
haftmann <none@none> |
basic documentation for computations
--HG--
extra : rebase_source : d93164fed6eb40c0d78779f72878f42feb87415b
|
| #
c8c848bc |
|
12-Dec-2016 |
wenzelm <none@none> |
proper session HOL-Types_To_Sets;
NEWS;
CONTRIBUTORS;
tuned whitespace;
|
| #
ac22f0ea |
|
31-Oct-2016 |
wenzelm <none@none> |
back to post-release mode -- after fork point;
|
| #
f3c6f689 |
|
31-Oct-2016 |
blanchet <none@none> |
moved contribution to right release
|
| #
2ad46537 |
|
24-Oct-2016 |
wenzelm <none@none> |
tuned and updated for release;
|
| #
49b2e8f2 |
|
24-Oct-2016 |
blanchet <none@none> |
added Nunchaku integration
|
| #
ef9c58ee |
|
24-Oct-2016 |
eberlm <eberlm@in.tum.de> |
Updated NEWS/CONTRIBUTORS w.r.t. Old_Number_Theory
|
| #
17a34890 |
|
07-Oct-2016 |
wenzelm <none@none> |
updated for release;
|
| #
b672e312 |
|
03-Oct-2016 |
haftmann <none@none> |
CONTRIBUTORS
--HG--
extra : rebase_source : fb6e9478a9e8db4da30e11a6b676185f7333a774
|
| #
0ee932e0 |
|
29-Sep-2016 |
boehmes <none@none> |
CONTRIBUTORS: new proof method "argo"
|
| #
ca80fd7f |
|
27-Jul-2016 |
Manuel Eberl <eberlm@in.tum.de> |
NEWS: Primes
|
| #
4fd0cb28 |
|
07-Jul-2016 |
nipkow <none@none> |
got rid of class cmp; added height-size proofs by Daniel Stuewe
|
| #
69b62cab |
|
08-Jun-2016 |
Andreas Lochbihler <none@none> |
NEWS and CONTRIBUTORS for SPMF
|
| #
2111cf75 |
|
27-Mar-2016 |
blanchet <none@none> |
tuning
|
| #
6a7f7b3f |
|
21-Mar-2016 |
blanchet <none@none> |
document addition of 'corec'
|
| #
7201ac81 |
|
18-Mar-2016 |
Andreas Lochbihler <none@none> |
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
|
| #
358358da |
|
03-Mar-2016 |
haftmann <none@none> |
constructive formulation of factorization
|
| #
6688eecc |
|
17-Feb-2016 |
haftmann <none@none> |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
| #
867505d5 |
|
23-Jan-2016 |
wenzelm <none@none> |
more CONTRIBUTORS;
|
| #
b0fe3086 |
|
20-Jan-2016 |
wenzelm <none@none> |
back to post-release mode -- after fork point;
|
| #
a41b972e |
|
19-Jan-2016 |
wenzelm <none@none> |
tuned;
|
| #
70cfb800 |
|
19-Jan-2016 |
Manuel Eberl <eberlm@in.tum.de> |
Added approximation of powr to NEWS/CONTRIBUTORS
|
| #
4918a15c |
|
12-Jan-2016 |
paulson <lp15@cam.ac.uk> |
crediting LCP in CONTRIBUTORS
|
| #
a3da8979 |
|
10-Jan-2016 |
kleing <none@none> |
print_record NEWS and CONTRIBUTORS
|
| #
ece32874 |
|
08-Jan-2016 |
wenzelm <none@none> |
tuned;
|
| #
bdc930da |
|
07-Jan-2016 |
Manuel Eberl <eberlm@in.tum.de> |
Added formal power series updates to NEWS/CONTRIBUTORS
|
| #
f52d581e |
|
06-Jan-2016 |
wenzelm <none@none> |
misc tuning for release;
|
| #
5ad25152 |
|
05-Jan-2016 |
hoelzl <none@none> |
add the proof of the central limit theorem
--HG--
extra : rebase_source : 493d99e28392771c51f4102a11b90533880e289f
extra : amend_source : 3fb7b7c607104e57a2c3ba7f733dd570eb42fa3b
|
| #
31fc9175 |
|
05-Jan-2016 |
wenzelm <none@none> |
misc tuning for release;
|
| #
1e2eaa87 |
|
05-Jan-2016 |
eberlm <none@none> |
Added summability/Gamma/etc. to NEWS and CONTRIBUTORS
|
| #
1ef22a74 |
|
31-Dec-2015 |
wenzelm <none@none> |
misc updates for release;
|
| #
a424472e |
|
19-Dec-2015 |
haftmann <none@none> |
documentation on last state of the art concerning interpretation
|
| #
f4c41fa6 |
|
30-Nov-2015 |
Andreas Lochbihler <none@none> |
add formalisation of Bourbaki-Witt fixpoint theorem
|
| #
dbea1757 |
|
02-Nov-2015 |
eberlm <none@none> |
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
|
| #
93f0bd28 |
|
12-Aug-2015 |
traytel <none@none> |
NEWS, CONTRIBUTORS, documentation for lift_bnf
|
| #
b553072c |
|
27-Jul-2015 |
haftmann <none@none> |
formal class for factorial (semi)rings
--HG--
extra : rebase_source : 5b8a7403f6fbaf86dcb8f95b0fd38d3c2225bb1e
|
| #
2a11bf54 |
|
08-Jul-2015 |
haftmann <none@none> |
moved normalization and unit_factor into Main HOL corpus
|
| #
20466aba |
|
02-Jul-2015 |
wenzelm <none@none> |
more CONTRIBUTORS;
|
| #
52933f0b |
|
18-Jun-2015 |
haftmann <none@none> |
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
--HG--
extra : rebase_source : 0045d1e39f330613bb1913e52e231f8be282a80a
|
| #
574107f8 |
|
12-Jun-2015 |
haftmann <none@none> |
CONTRIBUTORS
--HG--
extra : rebase_source : e6528886c4c38a5a16e3a3ca7c42b79329f84206
|
| #
2387db5d |
|
04-May-2015 |
wenzelm <none@none> |
tuned;
|
| #
f31e8fc1 |
|
04-May-2015 |
kuncar <none@none> |
CONTRIBUTORS
|
| #
1941baab |
|
19-Apr-2015 |
wenzelm <none@none> |
back to post-release mode -- after fork point;
|
| #
c5a56f5d |
|
17-Apr-2015 |
wenzelm <none@none> |
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
|
| #
ab90eabb |
|
11-Apr-2015 |
wenzelm <none@none> |
updated for release;
|
| #
be2e2524 |
|
08-Apr-2015 |
wenzelm <none@none> |
misc tuning for release;
|
| #
1a2350fc |
|
25-Mar-2015 |
blanchet <none@none> |
more multiset theorems
|
| #
2dd36018 |
|
04-Dec-2014 |
hoelzl <none@none> |
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
--HG--
extra : rebase_source : 8c7131ba8a4f577186bc3393e7116b70e552dd7e
|
| #
870e2a92 |
|
08-Oct-2014 |
Andreas Lochbihler <none@none> |
move Code_Test to HOL/Library;
add corresponding entries in NEWS and CONTRIBUTORS
--HG--
rename : src/HOL/Codegenerator_Test/Code_Test.thy => src/HOL/Library/Code_Test.thy
rename : src/HOL/Codegenerator_Test/code_test.ML => src/HOL/Library/code_test.ML
|
| #
b849aff1 |
|
06-Sep-2014 |
haftmann <none@none> |
theory about lexicographic ordering on functions
|
| #
347e01f2 |
|
22-Aug-2014 |
haftmann <none@none> |
generic euclidean algorithm (due to Manuel Eberl)
|
| #
117bc591 |
|
09-Aug-2014 |
wenzelm <none@none> |
tuned;
|
| #
70734c82 |
|
30-Jul-2014 |
wenzelm <none@none> |
CONTRIBUTORS;
|
| #
ed569d89 |
|
05-Jul-2014 |
haftmann <none@none> |
CONTRIBUTORS
|
| #
c2680fe6 |
|
05-Jul-2014 |
wenzelm <none@none> |
tuned;
|
| #
a00502b4 |
|
05-Jul-2014 |
kleing <none@none> |
added Tom's hyp_subst update
|
| #
d271aa2c |
|
01-Jul-2014 |
paulson <lp15@cam.ac.uk> |
for new release
|
| #
592c7699 |
|
01-Jul-2014 |
wenzelm <none@none> |
misc updates for release;
|
| #
91785aba |
|
28-Jun-2014 |
haftmann <none@none> |
CONTRIBUTORS
|
| #
4f8d73be |
|
27-Jul-2014 |
wenzelm <none@none> |
back to post-release mode -- after fork point;
|
| #
b0ac0132 |
|
16-Jun-2014 |
hoelzl <none@none> |
lemmas about the moments of the normal distribution
--HG--
extra : rebase_source : 614b198c1b9b5c3111bc69c44d5d82348aa23b61
|
| #
69ece7a6 |
|
13-Jun-2014 |
hoelzl <none@none> |
properties of normal distributed random variables (by Sudeep Kanav)
|
| #
33db321f |
|
12-Jun-2014 |
hoelzl <none@none> |
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
--HG--
extra : rebase_source : b821e7a52658fa32f598433901729ddc5fc949dd
|
| #
778ded51 |
|
11-Jun-2014 |
blanchet <none@none> |
updated contributors to include students
|
| #
b4e634d8 |
|
20-May-2014 |
blanchet <none@none> |
CONTRIBUTORS
|
| #
bd3d0c3a |
|
05-Apr-2014 |
haftmann <none@none> |
avoid romanism
|
| #
84205689 |
|
05-Apr-2014 |
haftmann <none@none> |
CONTRIBUTORS
|
| #
dcbb0326 |
|
13-Mar-2014 |
blanchet <none@none> |
updated NEWS and CONTRIBUTORS (BNF, SMT2, Sledgehammer)
|
| #
2334a365 |
|
05-Mar-2014 |
wenzelm <none@none> |
proper UTF-8;
|
| #
95c38159 |
|
04-Mar-2014 |
nipkow <none@none> |
added contributor
|
| #
6b0c03d3 |
|
04-Feb-2014 |
Lars Hupel <lars.hupel@mytum.de> |
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
--HG--
extra : amend_source : ecfd76d4e8277199ca35432e0682414689f265fb
|
| #
85cd5f87 |
|
05-Nov-2013 |
wenzelm <none@none> |
tuned;
|
| #
dbaafca8 |
|
28-Oct-2013 |
noschinl <none@none> |
CONTRIBUTORS
|
| #
ca012570 |
|
03-Oct-2013 |
wenzelm <none@none> |
back to post-release mode -- after fork point;
|
| #
df4e6c56 |
|
03-Oct-2013 |
wenzelm <none@none> |
tuned;
|
| #
07a55fa5 |
|
02-Oct-2013 |
wenzelm <none@none> |
tuned;
|
| #
ff59a45b |
|
02-Oct-2013 |
traytel <none@none> |
NEWS and CONTRIBUTORS
|
| #
2e36e9c3 |
|
02-Oct-2013 |
kuncar <none@none> |
typo
|
| #
56d15c42 |
|
02-Oct-2013 |
kuncar <none@none> |
NEWS and CONTRIBUTORS
|
| #
60e79d16 |
|
01-Oct-2013 |
blanchet <none@none> |
minor textual changes
|
| #
840514a1 |
|
29-Sep-2013 |
wenzelm <none@none> |
updated for release;
|
| #
75535ad5 |
|
28-Sep-2013 |
wenzelm <none@none> |
updated for release;
|
| #
6db2e90f |
|
20-Sep-2013 |
blanchet <none@none> |
updated CONTRIBUTORS
|
| #
4a292755 |
|
18-Sep-2013 |
blanchet <none@none> |
updated NEWS and CONTRIBUTORS
|
| #
d6b7dbf5 |
|
10-Sep-2013 |
krauss <none@none> |
NEWS and CONTRIBUTORS
|
| #
f110fb67 |
|
04-Sep-2013 |
wenzelm <none@none> |
more contributors;
|
| #
09ff74e7 |
|
29-Aug-2013 |
blanchet <none@none> |
updated news/contributors with BNF stuff
|
| #
2ccae8cc |
|
22-Aug-2013 |
wenzelm <none@none> |
clarified position of Spec_Check for Isabelle/ML -- it is unrelated to Isabelle/HOL;
just one src/Tools/ROOT;
--HG--
rename : src/HOL/Spec_Check/Examples.thy => src/Tools/Spec_Check/Examples.thy
rename : src/HOL/Spec_Check/README => src/Tools/Spec_Check/README
rename : src/HOL/Spec_Check/Spec_Check.thy => src/Tools/Spec_Check/Spec_Check.thy
rename : src/HOL/Spec_Check/base_generator.ML => src/Tools/Spec_Check/base_generator.ML
rename : src/HOL/Spec_Check/gen_construction.ML => src/Tools/Spec_Check/gen_construction.ML
rename : src/HOL/Spec_Check/generator.ML => src/Tools/Spec_Check/generator.ML
rename : src/HOL/Spec_Check/output_style.ML => src/Tools/Spec_Check/output_style.ML
rename : src/HOL/Spec_Check/property.ML => src/Tools/Spec_Check/property.ML
rename : src/HOL/Spec_Check/random.ML => src/Tools/Spec_Check/random.ML
rename : src/HOL/Spec_Check/spec_check.ML => src/Tools/Spec_Check/spec_check.ML
|
| #
533cc2fc |
|
07-Aug-2013 |
wenzelm <none@none> |
more NEWS and CONTRIBUTORS;
|
| #
a51866ba |
|
02-Jul-2013 |
wenzelm <none@none> |
tuned;
|
| #
a64a1b5b |
|
30-Jun-2013 |
haftmann <none@none> |
CONTRIBUTORS
|
| #
b313d78a |
|
30-May-2013 |
bulwahn <none@none> |
NEWS about Spec_Check
|
| #
89bf7cf4 |
|
10-Apr-2013 |
traytel <none@none> |
NEWS and CONTRIBUTORS
|
| #
d4cae3bf |
|
23-Mar-2013 |
haftmann <none@none> |
fundamental revision of big operators on sets
|
| #
a187bec2 |
|
23-Mar-2013 |
haftmann <none@none> |
locales for abstract orders
|
| #
6b8e5a08 |
|
17-Feb-2013 |
haftmann <none@none> |
Sieve of Eratosthenes
|
| #
20abf26b |
|
17-Feb-2013 |
haftmann <none@none> |
CONTRIBUTORS
--HG--
extra : rebase_source : 760a469c2e9f7a76a8b43a1a42c1fe251bb08302
|
| #
cc876414 |
|
20-Jan-2013 |
wenzelm <none@none> |
updated for release;
|
| #
5ca972cb |
|
20-Jan-2013 |
wenzelm <none@none> |
misc tuning for release;
|
| #
2f1c5762 |
|
20-Jan-2013 |
wenzelm <none@none> |
back to post-release mode -- after fork point;
|
| #
326e0990 |
|
31-Dec-2012 |
wenzelm <none@none> |
updated for release;
|
| #
9ef99d57 |
|
17-Dec-2012 |
nipkow <none@none> |
new contributor
|
| #
b49ee890 |
|
26-Nov-2012 |
blanchet <none@none> |
added file headers
|
| #
4ee9b475 |
|
26-Nov-2012 |
blanchet <none@none> |
updated NEWS etc.
|
| #
3b5de66a |
|
24-Nov-2012 |
wenzelm <none@none> |
more NEWS/CONTRIBUTORS;
|
| #
ef96acac |
|
21-Nov-2012 |
hoelzl <none@none> |
CONTRIBUTION: add fabians work
|
| #
215fe3f7 |
|
10-Oct-2012 |
Andreas Lochbihler <none@none> |
efficient construction of red black trees from sorted associative lists
|
| #
5eef42fd |
|
22-Sep-2012 |
wenzelm <none@none> |
some PIDE NEWS from this summer;
|
| #
54734983 |
|
21-Sep-2012 |
blanchet <none@none> |
renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"
--HG--
rename : src/HOL/Codatatype/BNF.thy => src/HOL/BNF/BNF.thy
rename : src/HOL/Codatatype/BNF_Comp.thy => src/HOL/BNF/BNF_Comp.thy
rename : src/HOL/Codatatype/BNF_Def.thy => src/HOL/BNF/BNF_Def.thy
rename : src/HOL/Codatatype/BNF_FP.thy => src/HOL/BNF/BNF_FP.thy
rename : src/HOL/Codatatype/BNF_GFP.thy => src/HOL/BNF/BNF_GFP.thy
rename : src/HOL/Codatatype/BNF_LFP.thy => src/HOL/BNF/BNF_LFP.thy
rename : src/HOL/Codatatype/BNF_Util.thy => src/HOL/BNF/BNF_Util.thy
rename : src/HOL/Codatatype/BNF_Wrap.thy => src/HOL/BNF/BNF_Wrap.thy
rename : src/HOL/Codatatype/Basic_BNFs.thy => src/HOL/BNF/Basic_BNFs.thy
rename : src/HOL/Codatatype/Countable_Set.thy => src/HOL/BNF/Countable_Set.thy
rename : src/HOL/Codatatype/Equiv_Relations_More.thy => src/HOL/BNF/Equiv_Relations_More.thy
rename : src/HOL/Codatatype/Examples/HFset.thy => src/HOL/BNF/Examples/HFset.thy
rename : src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Gram_Lang.thy => src/HOL/BNF/Examples/Infinite_Derivation_Trees/Gram_Lang.thy
rename : src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Parallel.thy => src/HOL/BNF/Examples/Infinite_Derivation_Trees/Parallel.thy
rename : src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Prelim.thy => src/HOL/BNF/Examples/Infinite_Derivation_Trees/Prelim.thy
rename : src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy => src/HOL/BNF/Examples/Infinite_Derivation_Trees/Tree.thy
rename : src/HOL/Codatatype/Examples/Lambda_Term.thy => src/HOL/BNF/Examples/Lambda_Term.thy
rename : src/HOL/Codatatype/Examples/ListF.thy => src/HOL/BNF/Examples/ListF.thy
rename : src/HOL/Codatatype/Examples/Misc_Codata.thy => src/HOL/BNF/Examples/Misc_Codata.thy
rename : src/HOL/Codatatype/Examples/Misc_Data.thy => src/HOL/BNF/Examples/Misc_Data.thy
rename : src/HOL/Codatatype/Examples/Process.thy => src/HOL/BNF/Examples/Process.thy
rename : src/HOL/Codatatype/Examples/Stream.thy => src/HOL/BNF/Examples/Stream.thy
rename : src/HOL/Codatatype/Examples/TreeFI.thy => src/HOL/BNF/Examples/TreeFI.thy
rename : src/HOL/Codatatype/Examples/TreeFsetI.thy => src/HOL/BNF/Examples/TreeFsetI.thy
rename : src/HOL/Codatatype/More_BNFs.thy => src/HOL/BNF/More_BNFs.thy
rename : src/HOL/Codatatype/README.html => src/HOL/BNF/README.html
rename : src/HOL/Codatatype/Tools/bnf_comp.ML => src/HOL/BNF/Tools/bnf_comp.ML
rename : src/HOL/Codatatype/Tools/bnf_comp_tactics.ML => src/HOL/BNF/Tools/bnf_comp_tactics.ML
rename : src/HOL/Codatatype/Tools/bnf_def.ML => src/HOL/BNF/Tools/bnf_def.ML
rename : src/HOL/Codatatype/Tools/bnf_def_tactics.ML => src/HOL/BNF/Tools/bnf_def_tactics.ML
rename : src/HOL/Codatatype/Tools/bnf_fp.ML => src/HOL/BNF/Tools/bnf_fp.ML
rename : src/HOL/Codatatype/Tools/bnf_fp_sugar.ML => src/HOL/BNF/Tools/bnf_fp_sugar.ML
rename : src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML => src/HOL/BNF/Tools/bnf_fp_sugar_tactics.ML
rename : src/HOL/Codatatype/Tools/bnf_gfp.ML => src/HOL/BNF/Tools/bnf_gfp.ML
rename : src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML => src/HOL/BNF/Tools/bnf_gfp_tactics.ML
rename : src/HOL/Codatatype/Tools/bnf_gfp_util.ML => src/HOL/BNF/Tools/bnf_gfp_util.ML
rename : src/HOL/Codatatype/Tools/bnf_lfp.ML => src/HOL/BNF/Tools/bnf_lfp.ML
rename : src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML => src/HOL/BNF/Tools/bnf_lfp_tactics.ML
rename : src/HOL/Codatatype/Tools/bnf_lfp_util.ML => src/HOL/BNF/Tools/bnf_lfp_util.ML
rename : src/HOL/Codatatype/Tools/bnf_tactics.ML => src/HOL/BNF/Tools/bnf_tactics.ML
rename : src/HOL/Codatatype/Tools/bnf_util.ML => src/HOL/BNF/Tools/bnf_util.ML
rename : src/HOL/Codatatype/Tools/bnf_wrap.ML => src/HOL/BNF/Tools/bnf_wrap.ML
rename : src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML => src/HOL/BNF/Tools/bnf_wrap_tactics.ML
|
| #
b0636b87 |
|
20-Sep-2012 |
Andreas Lochbihler <none@none> |
NEWS and CONTRIBUTORS for a5377f6d9f14 and f0ecc1550998
|
| #
2cc0ca92 |
|
07-Sep-2012 |
haftmann <none@none> |
lattice instances for option type
|
| #
1716e38d |
|
03-Sep-2012 |
Christian Sternagel <none@none> |
NEWS; CONTRIBUTORS
--HG--
extra : rebase_source : 41a9f8e45f70aa846d148a3f83be8865216274be
|
| #
2cad9214 |
|
28-Aug-2012 |
blanchet <none@none> |
updated NEWS and CONTRIBUTORS
|
| #
b321d029 |
|
28-Jul-2012 |
wenzelm <none@none> |
announce advanced support for Isabelle sessions and build management;
|
| #
79d7b708 |
|
25-Jun-2012 |
wenzelm <none@none> |
ignore morphism more explicitly;
tuned headers;
|
| #
b88d7767 |
|
21-Jun-2012 |
bulwahn <none@none> |
NEWS and CONTRIBUTORS
|
| #
77479094 |
|
02-May-2012 |
wenzelm <none@none> |
back to post-release mode -- after fork point;
|
| #
f46ac2a8 |
|
27-Apr-2012 |
wenzelm <none@none> |
tuned;
|
| #
9e94ba76 |
|
23-Apr-2012 |
kuncar <none@none> |
CONTRIBUTORS
|
| #
9f0949cf |
|
23-Apr-2012 |
hoelzl <none@none> |
CONTRIBUTORS
|
| #
fe6fc7a9 |
|
17-Apr-2012 |
Thomas Sewell <thomas.sewell@nicta.com.au> |
New tactic "word_bitwise" expands word equalities/inequalities into logic.
--HG--
extra : rebase_source : 8bdb429daca246ca01f6e7b8afb62076b340d329
|
| #
2eae14ab |
|
18-Apr-2012 |
blanchet <none@none> |
Sledgehammer NEWS and CONTRIBUTORS
|
| #
11a68501 |
|
15-Apr-2012 |
wenzelm <none@none> |
more CONTRIBUTORS;
|
| #
13e5e136 |
|
13-Apr-2012 |
wenzelm <none@none> |
some updates for release;
|
| #
4b7c4e48 |
|
13-Apr-2012 |
bulwahn <none@none> |
NEWS
|
| #
df6d30a0 |
|
10-Apr-2012 |
wenzelm <none@none> |
some coverage of HOL/TPTP;
|
| #
495168d2 |
|
01-Apr-2012 |
krauss <none@none> |
less modest NEWS; CONTRIBUTORS
|
| #
61f8ea4a |
|
23-Feb-2012 |
haftmann <none@none> |
CONTRIBUTORS
|
| #
3b0f7c18 |
|
26-Sep-2011 |
wenzelm <none@none> |
back to post-release mode;
|
| #
0fa4f3a6 |
|
18-Sep-2011 |
wenzelm <none@none> |
misc tuning for release;
|
| #
bbec29d8 |
|
12-Sep-2011 |
huffman <none@none> |
fix typo
|
| #
2dfc3970 |
|
12-Sep-2011 |
huffman <none@none> |
NEWS and CONTRIBUTORS
|
| #
e53decff |
|
12-Sep-2011 |
hoelzl <none@none> |
adding NEWS and CONTRIBUTORS
|
| #
97629975 |
|
12-Sep-2011 |
blanchet <none@none> |
added my contributions to NEWS and CONTRIBUTORS
|
| #
f33f6f14 |
|
12-Sep-2011 |
bulwahn <none@none> |
moving connection of association lists to Mappings into a separate theory
--HG--
rename : src/HOL/Library/AssocList.thy => src/HOL/Library/AList_Impl.thy
|
| #
80b9cc26 |
|
11-Sep-2011 |
wenzelm <none@none> |
more CONTRIBUTORS;
|
| #
c06e49a2 |
|
07-Sep-2011 |
haftmann <none@none> |
theory of saturated naturals contributed by Peter Gammie
|
| #
332aae5a |
|
07-Sep-2011 |
wenzelm <none@none> |
some updates for release;
|
| #
4091869d |
|
17-Jan-2011 |
wenzelm <none@none> |
back to post-release mode;
|
| #
b91248b9 |
|
16-Jan-2011 |
wenzelm <none@none> |
misc updates for release;
|
| #
6fbd82a8 |
|
14-Jan-2011 |
berghofe <none@none> |
Added entry for HOL-SPARK
|
| #
f5087030 |
|
12-Jan-2011 |
krauss <none@none> |
CONTRIBUTORS
|
| #
bfdb3d14 |
|
11-Jan-2011 |
wenzelm <none@none> |
updated to Isabelle2011;
|
| #
f4dc9a7d |
|
05-Nov-2010 |
wenzelm <none@none> |
proper spelling;
proper format;
|
| #
58779473 |
|
05-Nov-2010 |
hoelzl <none@none> |
Extend convex analysis by Bogdan Grechuk
|
| #
503ead12 |
|
29-Oct-2010 |
wenzelm <none@none> |
CONTRIBUTORS;
|
| #
7bfd5c01 |
|
25-Oct-2010 |
haftmann <none@none> |
CONTRIBUTORS
|
| #
9765a6b7 |
|
23-Sep-2010 |
haftmann <none@none> |
CONTRIBUTORS and NEWS
|
| #
2eca6769 |
|
23-Aug-2010 |
hoelzl <none@none> |
Rewrite the Probability theory.
Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.
--HG--
rename : src/HOL/Probability/Lebesgue.thy => src/HOL/Probability/Lebesgue_Integration.thy
|
| #
19854114 |
|
17-Aug-2010 |
haftmann <none@none> |
NEWS and CONTRIBUTORS
|
| #
6cb9ab58 |
|
07-Jun-2010 |
wenzelm <none@none> |
back to non-release mode;
|
| #
64031618 |
|
03-Jun-2010 |
krauss <none@none> |
CONTRIBUTORS
|
| #
7a2c1a3a |
|
02-Jun-2010 |
wenzelm <none@none> |
more CONTRIBUTORS;
|
| #
8265bb80 |
|
27-May-2010 |
wenzelm <none@none> |
misc updates for release;
|
| #
62ec3d5e |
|
27-Apr-2010 |
haftmann <none@none> |
NEWS and CONTRIBUTORS
|
| #
a416658a |
|
04-Dec-2009 |
wenzelm <none@none> |
back to after-release mode;
|
| #
b4b8fa54 |
|
25-Nov-2009 |
wenzelm <none@none> |
tuned affiliation;
|
| #
ce5d97ff |
|
24-Nov-2009 |
boehmes <none@none> |
extended list of HOL-Boogie contributors
|
| #
73747db6 |
|
23-Nov-2009 |
haftmann <none@none> |
CONTRIBUTORS
|
| #
8b4b14f6 |
|
22-Nov-2009 |
wenzelm <none@none> |
more NEWS, more tuning for release;
|
| #
e50c8c42 |
|
22-Nov-2009 |
wenzelm <none@none> |
misc tuning and updates for official release;
|
| #
474424ba |
|
19-Nov-2009 |
hoelzl <none@none> |
Added the contributions of Robert Himmelmann to CONTRIBUTIONS and NEWS
|
| #
45e21f32 |
|
12-Nov-2009 |
bulwahn <none@none> |
added a tabled implementation of the reflexive transitive closure
|
| #
b2c6f601 |
|
12-Nov-2009 |
bulwahn <none@none> |
announcing the predicate compiler in NEWS and CONTRIBUTORS
|
| #
eac3e3c8 |
|
03-Nov-2009 |
boehmes <none@none> |
added HOL-Boogie
|
| #
a2a8332f |
|
26-Oct-2009 |
wenzelm <none@none> |
misc tuning and updates;
|
| #
c17e22ae |
|
22-Oct-2009 |
blanchet <none@none> |
added Nitpick's theory and ML files to Isabelle/HOL;
the examples and the documentation are on their way.
|
| #
d3a3ef73 |
|
20-Oct-2009 |
boehmes <none@none> |
added proof reconstructon for Z3,
added certificates for simpler re-checking of proofs (no need to invoke external solvers),
added examples and certificates for all examples,
removed Unsynchronized.ref (in smt_normalize.ML)
|
| #
1e24fdd9 |
|
19-Oct-2009 |
haftmann <none@none> |
CONTRIBUTORS
|
| #
343a2f44 |
|
29-Sep-2009 |
wenzelm <none@none> |
Thomas Sewell, NICTA: more efficient HOL/record implementation;
|
| #
ebde388d |
|
18-Sep-2009 |
boehmes <none@none> |
added new method "smt": an oracle-based connection to external SMT solvers
|
| #
43de9743 |
|
17-Sep-2009 |
haftmann <none@none> |
tuned NEWS, added CONTRIBUTORS
|
| #
7d7803bc |
|
24-Jul-2009 |
Philipp Meyer <none@none> |
Functionality for sum of squares to call a remote csdp prover
|
| #
261728a4 |
|
14-Jul-2009 |
haftmann <none@none> |
NEWS and CONTRIBUTORS
|
| #
684c38d2 |
|
05-Jun-2009 |
haftmann <none@none> |
CONTRIBUTORS
|
| #
62e7a2f6 |
|
25-Apr-2009 |
wenzelm <none@none> |
post Isabelle2009 version;
|
| #
58208939 |
|
08-Apr-2009 |
wenzelm <none@none> |
updated official title of contribution by Johannes Hoelzl;
|
| #
e6fc9e5a |
|
09-Mar-2009 |
wenzelm <none@none> |
more contributors;
|
| #
0d4fc83b |
|
28-Feb-2009 |
wenzelm <none@none> |
A Serbian theory, by Filip Maric.
|
| #
c1d402c7 |
|
28-Feb-2009 |
wenzelm <none@none> |
more CONTRIBUTORS;
fixed some dates;
|
| #
daaec2e2 |
|
27-Feb-2009 |
wenzelm <none@none> |
more CONTRIBUTORS;
|
| #
f58ddbd6 |
|
12-Feb-2009 |
kleing <none@none> |
added find_consts to NEWS and CONTRIBUTORS
|
| #
c3237b34 |
|
11-Feb-2009 |
kleing <none@none> |
updated NEWS etc with "solves" criterion and auto_solves
|
| #
6f9ffb42 |
|
08-Jan-2009 |
haftmann <none@none> |
NEWS and CONTRIBUTORS
|
| #
aae55924 |
|
27-Dec-2008 |
krauss <none@none> |
tuned NEWS; CONTRIBUTORS
|
| #
66353221 |
|
20-Dec-2008 |
wenzelm <none@none> |
removed Ids;
|
| #
498bfeca |
|
28-Nov-2008 |
kleing <none@none> |
added Tim's find_theorems performance patch
|
| #
8b8616ea |
|
15-Oct-2008 |
wenzelm <none@none> |
generic ATP manager based on threads (by Fabian Immler);
|
| #
d55420dc |
|
03-Oct-2008 |
wenzelm <none@none> |
Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
|
| #
f2222726 |
|
28-May-2008 |
wenzelm <none@none> |
more contribs;
|
| #
2b2647a5 |
|
12-May-2008 |
wenzelm <none@none> |
misc tuning;
|
| #
43944ad9 |
|
22-Apr-2008 |
haftmann <none@none> |
added entries
|
| #
de832489 |
|
05-Mar-2008 |
wenzelm <none@none> |
HOL/Library/RBT.thy;
|
| #
154b1efd |
|
26-Nov-2007 |
wenzelm <none@none> |
Peter Lammich: HOL-Lattice lemmas;
|
| #
b5f3f912 |
|
21-Nov-2007 |
wenzelm <none@none> |
tuned;
|
| #
477d1aab |
|
20-Nov-2007 |
wenzelm <none@none> |
tuned;
|
| #
8a87a413 |
|
12-Nov-2007 |
schirmer <none@none> |
fixed typo;
|
| #
be423816 |
|
11-Nov-2007 |
wenzelm <none@none> |
HOL-Statespace;
|
| #
ee001ba8 |
|
16-Oct-2007 |
wenzelm <none@none> |
Mark A. Hillebrand, DFKI: Robust sub/superscripts in LaTeX document output.
|
| #
56c0ec59 |
|
01-Oct-2007 |
wenzelm <none@none> |
Norbert Schirmer: record improvements;
|
| #
6ba0afb0 |
|
01-Oct-2007 |
wenzelm <none@none> |
misc tuning and update;
|
| #
202d2a72 |
|
19-Aug-2007 |
kleing <none@none> |
* HOL-Word:
New extensive library and type for generic, fixed size machine
words, with arithemtic, bit-wise, shifting and rotating operations,
reflection into int, nat, and bool lists, automation for linear
arithmetic (by automatic reflection into nat or int), including
lemmas on overflow and monotonicity. Instantiated to all appropriate
arithmetic type classes, supporting automatic simplification of
numerals on all operations. Jointly developed by NICTA, Galois, and
PSU.
* still to do: README.html/document + moving some of the generic lemmas
to appropriate place in distribution
|
| #
ab4d3f6f |
|
19-Aug-2007 |
kleing <none@none> |
boolean algebras as locales and numbers as types by Brian Huffman
|
| #
e13d425a |
|
21-Jun-2007 |
paulson <none@none> |
integration of Metis prover
|
| #
2d263cf8 |
|
14-Jun-2007 |
kleing <none@none> |
clarified who we consider to be a contributor
|
| #
1c59e7f4 |
|
05-Jun-2007 |
wenzelm <none@none> |
Semiring normalization and Groebner Bases.
|
| #
9b473444 |
|
16-Mar-2007 |
haftmann <none@none> |
updated
|
| #
d093c321 |
|
08-Nov-2006 |
wenzelm <none@none> |
* November 2006: Lukas Bulwahn, TUM -- HOL/function: method "lexicographic_order".
|
| #
9cd3e666 |
|
04-Nov-2006 |
wenzelm <none@none> |
* October 2006: Stefan Hohe, TUM;
|
| #
4ee1ec6d |
|
05-Aug-2006 |
wenzelm <none@none> |
Amine Chaieb: experimental generic reflection and reification in HOL;
|
| #
3db2c959 |
|
10-Jul-2006 |
kleing <none@none> |
hex and binary numerals (contributed by Rafal Kolanski)
|
| #
99b33bb8 |
|
15-Jun-2006 |
nipkow <none@none> |
*** empty log message ***
|
| #
9333e641 |
|
16-May-2006 |
wenzelm <none@none> |
Amine Chaieb: Ferrante and Rackoff Algorithm;
|
| #
ef849276 |
|
25-Apr-2006 |
kleing <none@none> |
added Ben Porter's stuff
|
| #
30943ec1 |
|
14-Oct-2005 |
wenzelm <none@none> |
more;
|
| #
277f7107 |
|
25-Sep-2005 |
wenzelm <none@none> |
more;
|
| #
bfa0b1ea |
|
21-Sep-2005 |
wenzelm <none@none> |
tuned;
|
| #
c87d5754 |
|
21-Sep-2005 |
wenzelm <none@none> |
tuned;
|
| #
b3509f02 |
|
21-Sep-2005 |
wenzelm <none@none> |
tuned;
|
| #
d323a726 |
|
20-Sep-2005 |
wenzelm <none@none> |
HOL/ex/Chinese.thy;
|
| #
ec3db7af |
|
20-Sep-2005 |
wenzelm <none@none> |
more contributions;
|
| #
b689c508 |
|
14-Sep-2005 |
wenzelm <none@none> |
Bernhard Haeupler: comm_ring;
|
| #
50a07010 |
|
19-Jul-2005 |
wenzelm <none@none> |
more contribs;
|
| #
2ea8c061 |
|
18-Jul-2005 |
haftmann <none@none> |
reverted from fold_yield to fold_map
|
| #
02175d90 |
|
15-Jul-2005 |
wenzelm <none@none> |
*** empty log message ***
|
| #
f2ccb624 |
|
05-Jun-2005 |
wenzelm <none@none> |
Lucas Dixon;
|
| #
0fe3e9fd |
|
17-May-2005 |
wenzelm <none@none> |
proper Id line;
|
| #
503f70aa |
|
17-May-2005 |
wenzelm <none@none> |
updated;
|
| #
422f5eb2 |
|
17-May-2005 |
wenzelm <none@none> |
added;
|