Commit f261d5ea authored by Gerwin Klein's avatar Gerwin Klein

2021 web pages

parent 79150f043fa8
......@@ -184,7 +184,13 @@ security guarantees.</td>
<tr><td class="links">Older releases:
None
<ul>
<li>Isabelle 2020:
<a href="../release/afp-ADS_Functor-2020-04-27.tar.gz">
afp-ADS_Functor-2020-04-27.tar.gz
</a>
</li>
</ul>
</td></tr>
</tbody>
......
......@@ -176,7 +176,13 @@ formalisation in this entry was described in an earlier publication.</td>
<tr><td class="links">Older releases:
None
<ul>
<li>Isabelle 2020:
<a href="../release/afp-AI_Planning_Languages_Semantics-2020-10-30.tar.gz">
afp-AI_Planning_Languages_Semantics-2020-10-30.tar.gz
</a>
</li>
</ul>
</td></tr>
</tbody>
......
......@@ -192,7 +192,12 @@ automatically and identify exactly the steps that are no longer valid.
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-AODV-2020-04-18.tar.gz">
afp-AODV-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-AODV-2019-06-11.tar.gz">
afp-AODV-2019-06-11.tar.gz
</a>
......
......@@ -165,7 +165,12 @@ MathJax = {
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-AVL-Trees-2020-04-18.tar.gz">
afp-AVL-Trees-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-AVL-Trees-2019-06-11.tar.gz">
afp-AVL-Trees-2019-06-11.tar.gz
</a>
......
......@@ -193,7 +193,12 @@ terms and joining processes).</p></td>
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-AWN-2020-04-18.tar.gz">
afp-AWN-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-AWN-2019-06-11.tar.gz">
afp-AWN-2019-06-11.tar.gz
</a>
......
......@@ -175,7 +175,12 @@ refinement proof in the I/O-automata framework of Lynch and Tuttle.</td>
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-Abortable_Linearizable_Modules-2020-04-18.tar.gz">
afp-Abortable_Linearizable_Modules-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-Abortable_Linearizable_Modules-2019-06-11.tar.gz">
afp-Abortable_Linearizable_Modules-2019-06-11.tar.gz
</a>
......
......@@ -178,7 +178,12 @@ polished) development is covered in the book
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-Abs_Int_ITP2012-2020-04-18.tar.gz">
afp-Abs_Int_ITP2012-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-Abs_Int_ITP2012-2019-06-11.tar.gz">
afp-Abs_Int_ITP2012-2019-06-11.tar.gz
</a>
......
......@@ -162,7 +162,12 @@ MathJax = {
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-Abstract-Hoare-Logics-2020-04-18.tar.gz">
afp-Abstract-Hoare-Logics-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-Abstract-Hoare-Logics-2019-06-11.tar.gz">
afp-Abstract-Hoare-Logics-2019-06-11.tar.gz
</a>
......
......@@ -182,7 +182,12 @@ instances. <br>
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-Abstract-Rewriting-2020-04-18.tar.gz">
afp-Abstract-Rewriting-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-Abstract-Rewriting-2019-06-11.tar.gz">
afp-Abstract-Rewriting-2019-06-11.tar.gz
</a>
......
......@@ -167,7 +167,12 @@ The abstract proof can be instantiated for a wide range of Gentzen and tableau s
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-Abstract_Completeness-2020-04-18.tar.gz">
afp-Abstract_Completeness-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-Abstract_Completeness-2019-06-11.tar.gz">
afp-Abstract_Completeness-2019-06-11.tar.gz
</a>
......
......@@ -172,7 +172,12 @@ predicates.</td>
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-Abstract_Soundness-2020-04-18.tar.gz">
afp-Abstract_Soundness-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-Abstract_Soundness-2019-06-11.tar.gz">
afp-Abstract_Soundness-2019-06-11.tar.gz
</a>
......
......@@ -185,7 +185,12 @@ simple WHILE-language and its correctness is shown using Hoare-logic.</td>
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-Adaptive_State_Counting-2020-04-18.tar.gz">
afp-Adaptive_State_Counting-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-Adaptive_State_Counting-2019-08-19.tar.gz">
afp-Adaptive_State_Counting-2019-08-19.tar.gz
</a>
......
......@@ -174,7 +174,12 @@ type</td>
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-Affine_Arithmetic-2020-04-18.tar.gz">
afp-Affine_Arithmetic-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-Affine_Arithmetic-2019-06-11.tar.gz">
afp-Affine_Arithmetic-2019-06-11.tar.gz
</a>
......
......@@ -169,7 +169,12 @@ based on linearly ordered commutative semigroups.</td>
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-Aggregation_Algebras-2020-04-18.tar.gz">
afp-Aggregation_Algebras-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-Aggregation_Algebras-2019-06-11.tar.gz">
afp-Aggregation_Algebras-2019-06-11.tar.gz
</a>
......
......@@ -183,7 +183,12 @@ proof methods, see the accompanying paper (publication forthcoming).</td>
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-Akra_Bazzi-2020-04-18.tar.gz">
afp-Akra_Bazzi-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-Akra_Bazzi-2019-06-11.tar.gz">
afp-Akra_Bazzi-2019-06-11.tar.gz
</a>
......
......@@ -186,7 +186,12 @@ To this end, we mechanized several results on resultants, which also required us
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-Algebraic_Numbers-2020-04-18.tar.gz">
afp-Algebraic_Numbers-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-Algebraic_Numbers-2019-06-11.tar.gz">
afp-Algebraic_Numbers-2019-06-11.tar.gz
</a>
......
......@@ -189,7 +189,12 @@ trace semantics into the weakest precondition component.</td>
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-Algebraic_VCs-2020-04-18.tar.gz">
afp-Algebraic_VCs-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-Algebraic_VCs-2019-06-11.tar.gz">
afp-Algebraic_VCs-2019-06-11.tar.gz
</a>
......
......@@ -178,7 +178,12 @@ pages 528–531, 1985.</td>
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-Allen_Calculus-2020-04-18.tar.gz">
afp-Allen_Calculus-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-Allen_Calculus-2019-06-28.tar.gz">
afp-Allen_Calculus-2019-06-28.tar.gz
</a>
......
......@@ -166,7 +166,13 @@ Riele's Rule and Borho's Rule with breeders.</td>
<tr><td class="links">Older releases:
None
<ul>
<li>Isabelle 2020:
<a href="../release/afp-Amicable_Numbers-2020-08-15.tar.gz">
afp-Amicable_Numbers-2020-08-15.tar.gz
</a>
</li>
</ul>
</td></tr>
</tbody>
......
......@@ -182,7 +182,12 @@ is available <a href="http://www21.in.tum.de/~nipkow/pubs/jfp16.html">here</a>.<
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-Amortized_Complexity-2020-04-18.tar.gz">
afp-Amortized_Complexity-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-Amortized_Complexity-2019-06-11.tar.gz">
afp-Amortized_Complexity-2019-06-11.tar.gz
</a>
......
......@@ -168,7 +168,12 @@ Isabelle/HOL.</td>
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-AnselmGod-2020-04-18.tar.gz">
afp-AnselmGod-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-AnselmGod-2019-06-11.tar.gz">
afp-AnselmGod-2019-06-11.tar.gz
</a>
......
......@@ -179,7 +179,12 @@ improved compatibility with locale interpretation
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-Applicative_Lifting-2020-04-18.tar.gz">
afp-Applicative_Lifting-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-Applicative_Lifting-2019-06-11.tar.gz">
afp-Applicative_Lifting-2019-06-11.tar.gz
</a>
......
......@@ -170,7 +170,12 @@ A detailed description of our work has been published in the proceedings of
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-Approximation_Algorithms-2020-04-18.tar.gz">
afp-Approximation_Algorithms-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-Approximation_Algorithms-2020-01-16.tar.gz">
afp-Approximation_Algorithms-2020-01-16.tar.gz
</a>
......
......@@ -189,7 +189,12 @@ theory of architectural design patterns.</td>
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-Architectural_Design_Patterns-2020-04-18.tar.gz">
afp-Architectural_Design_Patterns-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-Architectural_Design_Patterns-2019-06-11.tar.gz">
afp-Architectural_Design_Patterns-2019-06-11.tar.gz
</a>
......
......@@ -173,7 +173,12 @@ Sledgehammer for simple exercises in philosophy.</td>
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-Aristotles_Assertoric_Syllogistic-2020-04-18.tar.gz">
afp-Aristotles_Assertoric_Syllogistic-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-Aristotles_Assertoric_Syllogistic-2019-10-17.tar.gz">
afp-Aristotles_Assertoric_Syllogistic-2019-10-17.tar.gz
</a>
......
......@@ -173,7 +173,12 @@ arithmetic progression?</td>
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-Arith_Prog_Rel_Primes-2020-04-18.tar.gz">
afp-Arith_Prog_Rel_Primes-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-Arith_Prog_Rel_Primes-2020-02-10.tar.gz">
afp-Arith_Prog_Rel_Primes-2020-02-10.tar.gz
</a>
......
......@@ -162,7 +162,12 @@ MathJax = {
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-ArrowImpossibilityGS-2020-04-18.tar.gz">
afp-ArrowImpossibilityGS-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-ArrowImpossibilityGS-2019-06-11.tar.gz">
afp-ArrowImpossibilityGS-2019-06-11.tar.gz
</a>
......
......@@ -167,7 +167,12 @@ elementary number theory of primes.</td>
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-Auto2_HOL-2020-04-18.tar.gz">
afp-Auto2_HOL-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-Auto2_HOL-2019-06-11.tar.gz">
afp-Auto2_HOL-2019-06-11.tar.gz
</a>
......
......@@ -178,7 +178,12 @@ working with separation logic.</td>
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-Auto2_Imperative_HOL-2020-04-18.tar.gz">
afp-Auto2_Imperative_HOL-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-Auto2_Imperative_HOL-2019-06-11.tar.gz">
afp-Auto2_Imperative_HOL-2019-06-11.tar.gz
</a>
......
......@@ -174,7 +174,12 @@ MathJax = {
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-AutoFocus-Stream-2020-04-18.tar.gz">
afp-AutoFocus-Stream-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-AutoFocus-Stream-2019-06-11.tar.gz">
afp-AutoFocus-Stream-2019-06-11.tar.gz
</a>
......
......@@ -176,7 +176,13 @@ specification language that is embedded into Isabelle.</td>
<tr><td class="links">Older releases:
None
<ul>
<li>Isabelle 2020:
<a href="../release/afp-Automated_Stateful_Protocol_Verification-2020-05-20.tar.gz">
afp-Automated_Stateful_Protocol_Verification-2020-05-20.tar.gz
</a>
</li>
</ul>
</td></tr>
</tbody>
......
......@@ -176,7 +176,12 @@ the nondeterminism monad and various collection datastructures.</td>
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-Automatic_Refinement-2020-04-18.tar.gz">
afp-Automatic_Refinement-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-Automatic_Refinement-2019-06-11.tar.gz">
afp-Automatic_Refinement-2019-06-11.tar.gz
</a>
......
......@@ -183,7 +183,12 @@ minor technical issue.</td>
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-AxiomaticCategoryTheory-2020-04-18.tar.gz">
afp-AxiomaticCategoryTheory-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-AxiomaticCategoryTheory-2019-06-11.tar.gz">
afp-AxiomaticCategoryTheory-2019-06-11.tar.gz
</a>
......
......@@ -163,7 +163,12 @@ MathJax = {
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-BDD-2020-04-18.tar.gz">
afp-BDD-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-BDD-2019-06-11.tar.gz">
afp-BDD-2019-06-11.tar.gz
</a>
......
......@@ -189,7 +189,12 @@ BNF<sub>CC</sub> theory to several concrete functors.</td>
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-BNF_CC-2020-04-18.tar.gz">
afp-BNF_CC-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-BNF_CC-2019-06-11.tar.gz">
afp-BNF_CC-2019-06-11.tar.gz
</a>
......
......@@ -178,7 +178,12 @@ N2M operation provides mutual (co)induction principles and
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-BNF_Operations-2020-04-18.tar.gz">
afp-BNF_Operations-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-BNF_Operations-2019-06-11.tar.gz">
afp-BNF_Operations-2019-06-11.tar.gz
</a>
......
......@@ -166,7 +166,18 @@ adaptation to Isabelle/HOL of a proof due to A. Sokal.</td>
<tr><td class="links">Older releases:
None
<ul>
<li>Isabelle 2020:
<a href="../release/afp-Banach_Steinhaus-2020-05-11.tar.gz">
afp-Banach_Steinhaus-2020-05-11.tar.gz
</a>
</li>
<li>Isabelle 2020:
<a href="../release/afp-Banach_Steinhaus-2020-05-06.tar.gz">
afp-Banach_Steinhaus-2020-05-06.tar.gz
</a>
</li>
</ul>
</td></tr>
</tbody>
......
......@@ -185,7 +185,12 @@ predicates and rules, and follows a repeating structure in its Isar proof.</td>
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-Bell_Numbers_Spivey-2020-04-18.tar.gz">
afp-Bell_Numbers_Spivey-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-Bell_Numbers_Spivey-2019-06-11.tar.gz">
afp-Bell_Numbers_Spivey-2019-06-11.tar.gz
</a>
......
......@@ -191,7 +191,12 @@ local type definitions.
<tr><td class="links">Older releases:
<ul>
<li>Isabelle 2019:
<li>Isabelle 2020:
<a href="../release/afp-Berlekamp_Zassenhaus-2020-04-18.tar.gz">
afp-Berlekamp_Zassenhaus-2020-04-18.tar.gz
</a>
</li>
<li>Isabelle 2019:
<a href="../release/afp-Berlekamp_Zassenhaus-2019-06-11.tar.gz">
afp-Berlekamp_Zassenhaus-2019-06-11.tar.gz
</a>
......
......@@ -180,7 +180,12 @@ prove their basic properties.</p></td>