diff --git a/etc/version b/etc/version --- a/etc/version +++ b/etc/version @@ -1,4 +1,4 @@ # -*- shell-script -*- # AFP version of this repository ("devel" or "2016-1", "2017" etc) -VERSION=devel +VERSION=2021 diff --git a/metadata/templates/using.tpl b/metadata/templates/using.tpl --- a/metadata/templates/using.tpl +++ b/metadata/templates/using.tpl @@ -1,50 +1,50 @@ {% extends "base.tpl" %} {% block headline %} Referring to AFP Entries {% endblock %} {% block content %}

Once you have downloaded the AFP, you can include its articles and theories in your own developments. If you would like to make your work available to others without having to include the AFP articles you depend on, here is how to do it.

-If you are using Isabelle2020, and have downloaded your AFP directory to +If you are using Isabelle2021, and have downloaded your AFP directory to /home/myself/afp, you should run the following command [1] to make the AFP session ROOTS available to Isabelle:

-    echo "/home/myself/afp/thys" >> ~/.isabelle/Isabelle2020/ROOTS
+    echo "/home/myself/afp/thys" >> ~/.isabelle/Isabelle2021/ROOTS
 

You can now refer to article ABC from the AFP in some theory of yours via

     imports "ABC.Some_ABC_Theory"
 

This allows you to distribute your material separately from any AFP theories. Users of your distribution also need to install the AFP in the above manner.

 

[1]: Tested for Linux and Mac installations ‐ it should be the same under cygwin on Windows.

{% endblock %} diff --git a/web/entries/Ergodic_Theory.html b/web/entries/Ergodic_Theory.html --- a/web/entries/Ergodic_Theory.html +++ b/web/entries/Ergodic_Theory.html @@ -1,207 +1,215 @@ Ergodic Theory - Archive of Formal Proofs

 

 

 

 

 

 

Ergodic Theory

 

+ + + +
Title: Ergodic Theory
Author: Sebastien Gouezel
+ Contributor: + + Manuel Eberl +
Submission date: 2015-12-01
Abstract: Ergodic theory is the branch of mathematics that studies the behaviour of measure preserving transformations, in finite or infinite measure. It interacts both with probability theory (mainly through measure theory) and with geometry as a lot of interesting examples are from geometric origin. We implement the first definitions and theorems of ergodic theory, including notably Poicaré recurrence theorem for finite measure preserving systems (together with the notion of conservativity in general), induced maps, Kac's theorem, Birkhoff theorem (arguably the most important theorem in ergodic theory), and variations around it such as conservativity of the corresponding skew product, or Atkinson lemma.
BibTeX:
@article{Ergodic_Theory-AFP,
   author  = {Sebastien Gouezel},
   title   = {Ergodic Theory},
   journal = {Archive of Formal Proofs},
   month   = dec,
   year    = 2015,
   note    = {\url{https://isa-afp.org/entries/Ergodic_Theory.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Used by: Gromov_Hyperbolicity, Laws_of_Large_Numbers, Lp

\ No newline at end of file diff --git a/web/statistics.html b/web/statistics.html --- a/web/statistics.html +++ b/web/statistics.html @@ -1,302 +1,302 @@ Archive of Formal Proofs

 

 

 

 

 

 

Statistics

 

Statistics

Number of Articles:582
Number of Authors:374
Number of lemmas:~163,500
Lines of Code:~2,854,400

Most used AFP articles:

NameUsed by ? articles
1. List-Index 17
2. Coinductive 12
Collections 12
Regular-Sets 12
3. Landau_Symbols 11
Show 11
4. Polynomial_Factorization 10
5. Abstract-Rewriting 9
Automatic_Refinement 9
Deriving 9
Jordan_Normal_Form 9

Growth in number of articles:

Growth in lines of code:

Growth in number of authors:

Size of articles:

\ No newline at end of file diff --git a/web/using.html b/web/using.html --- a/web/using.html +++ b/web/using.html @@ -1,118 +1,118 @@ Archive of Formal Proofs

 

 

 

 

 

 

Referring to AFP Entries

 

Once you have downloaded the AFP, you can include its articles and theories in your own developments. If you would like to make your work available to others without having to include the AFP articles you depend on, here is how to do it.

-If you are using Isabelle2020, and have downloaded your AFP directory to +If you are using Isabelle2021, and have downloaded your AFP directory to /home/myself/afp, you should run the following command [1] to make the AFP session ROOTS available to Isabelle:

-    echo "/home/myself/afp/thys" >> ~/.isabelle/Isabelle2020/ROOTS
+    echo "/home/myself/afp/thys" >> ~/.isabelle/Isabelle2021/ROOTS
 

You can now refer to article ABC from the AFP in some theory of yours via

     imports "ABC.Some_ABC_Theory"
 

This allows you to distribute your material separately from any AFP theories. Users of your distribution also need to install the AFP in the above manner.

 

[1]: Tested for Linux and Mac installations ‐ it should be the same under cygwin on Windows.

\ No newline at end of file