Commit 096ef60b authored by Lars Hupel's avatar Lars Hupel
Browse files

regenerate entries

--HG--
branch : depends-on
parent 9c0b6d5f7093
......@@ -86,6 +86,10 @@ automatically and identify exactly the steps that are no longer valid.
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="AWN.shtml">AWN</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -82,6 +82,10 @@ instances. <br>
<td class="data"><a href="http://afp.sourceforge.net/LICENSE.LGPL">GNU Lesser General Public License (LGPL)</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Regular-Sets.shtml">Regular-Sets</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -64,6 +64,10 @@ The abstract proof can be instantiated for a wide range of Gentzen and tableau s
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Collections.shtml">Collections</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -75,7 +75,7 @@ To this end, we mechanized several results on resultants, which also required us
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Sturm_Sequences.shtml">Sturm_Sequences</a>, <a href="Partial_Function_MR.shtml">Partial_Function_MR</a>, <a href="Sqrt_Babylonian.shtml">Sqrt_Babylonian</a>, <a href="Show.shtml">Show</a>, <a href="Jordan_Normal_Form.shtml">Jordan_Normal_Form</a>, <a href="Deriving.shtml">Deriving</a>, <a href="Polynomial_Factorization.shtml">Polynomial_Factorization</a></td></tr>
<td class="data"><a href="Sturm_Sequences.shtml">Sturm_Sequences</a>, <a href="Show.shtml">Show</a>, <a href="Deriving.shtml">Deriving</a>, <a href="Polynomial_Interpolation.shtml">Polynomial_Interpolation</a>, <a href="Abstract-Rewriting.shtml">Abstract-Rewriting</a>, <a href="Jordan_Normal_Form.shtml">Jordan_Normal_Form</a>, <a href="Polynomial_Factorization.shtml">Polynomial_Factorization</a>, <a href="Containers.shtml">Containers</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -78,7 +78,7 @@ Theorem Proving ITP 2015.
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Splay_Tree.shtml">Splay_Tree</a>, <a href="Skew_Heap.shtml">Skew_Heap</a></td></tr>
<td class="data"><a href="Splay_Tree.shtml">Splay_Tree</a>, <a href="Skew_Heap.shtml">Skew_Heap</a>, <a href="List-Index.shtml">List-Index</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -69,6 +69,10 @@ We formalize the AutoFocus Semantics (a time-synchronous subset of the Focus for
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="List-Infinite.shtml">List-Infinite</a>, <a href="Nat-Interval-Logic.shtml">Nat-Interval-Logic</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -90,7 +90,7 @@ CAVA Automata Library, Isabelle Workshop 2014.
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Collections.shtml">Collections</a></td></tr>
<td class="data"><a href="Collections.shtml">Collections</a>, <a href="Native_Word.shtml">Native_Word</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -85,7 +85,7 @@ with the same title.
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Gabow_SCC.shtml">Gabow_SCC</a>, <a href="Promela.shtml">Promela</a>, <a href="LTL_to_GBA.shtml">LTL_to_GBA</a></td></tr>
<td class="data"><a href="CAVA_Automata.shtml">CAVA_Automata</a>, <a href="Gabow_SCC.shtml">Gabow_SCC</a>, <a href="Promela.shtml">Promela</a>, <a href="LTL_to_GBA.shtml">LTL_to_GBA</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -90,6 +90,10 @@ was added.
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Launchbury.shtml">Launchbury</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -64,7 +64,7 @@ This entry provides several monads intended for the development of stand-alone c
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Show.shtml">Show</a>, <a href="Partial_Function_MR.shtml">Partial_Function_MR</a></td></tr>
<td class="data"><a href="Partial_Function_MR.shtml">Partial_Function_MR</a>, <a href="Show.shtml">Show</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -82,6 +82,10 @@ without further ado.</p>
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Regular-Sets.shtml">Regular-Sets</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -88,7 +88,7 @@ A compatibility file CollectionsV1 tries to simplify porting of existing theorie
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Binomial-Heaps.shtml">Binomial-Heaps</a>, <a href="Finger-Trees.shtml">Finger-Trees</a>, <a href="Refine_Monadic.shtml">Refine_Monadic</a></td></tr>
<td class="data"><a href="Finger-Trees.shtml">Finger-Trees</a>, <a href="Native_Word.shtml">Native_Word</a>, <a href="Trie.shtml">Trie</a>, <a href="Automatic_Refinement.shtml">Automatic_Refinement</a>, <a href="Refine_Monadic.shtml">Refine_Monadic</a>, <a href="Binomial-Heaps.shtml">Binomial-Heaps</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -79,6 +79,10 @@ algorithms, and classify them based on those choices.
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Heard_Of.shtml">Heard_Of</a>, <a href="Stuttering_Equivalence.shtml">Stuttering_Equivalence</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -84,7 +84,7 @@ provide generators for canonical type class instantiations
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Deriving.shtml">Deriving</a></td></tr>
<td class="data"><a href="Deriving.shtml">Deriving</a>, <a href="Collections.shtml">Collections</a>, <a href="Regular-Sets.shtml">Regular-Sets</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -80,7 +80,7 @@ command.
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Collections.shtml">Collections</a>, <a href="Deriving.shtml">Deriving</a></td></tr>
<td class="data"><a href="Deriving.shtml">Deriving</a>, <a href="Collections.shtml">Collections</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -65,7 +65,7 @@ This theory formalizes the commutation version of decreasing diagrams for Church
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Abstract-Rewriting.shtml">Abstract-Rewriting</a></td></tr>
<td class="data"><a href="Well_Quasi_Orders.shtml">Well_Quasi_Orders</a>, <a href="Abstract-Rewriting.shtml">Abstract-Rewriting</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -72,10 +72,6 @@ theorem and was therefore only proven for real polynomials.
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Sturm_Tarski.shtml">Sturm_Tarski</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -70,7 +70,7 @@ structures from the Isabelle Collection Framework.
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Refine_Monadic.shtml">Refine_Monadic</a>, <a href="Collections.shtml">Collections</a></td></tr>
<td class="data"><a href="Collections.shtml">Collections</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -63,6 +63,10 @@ We formalize an algorithm to compute the Echelon Form of a matrix. We have prove
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Gauss_Jordan.shtml">Gauss_Jordan</a>, <a href="Cayley_Hamilton.shtml">Cayley_Hamilton</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -68,6 +68,10 @@ This theorem is the 45th theorem of the Top 100 Theorems list.
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Card_Number_Partitions.shtml">Card_Number_Partitions</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -73,7 +73,7 @@ Brzozowski's minimization algorithm. Uniqueness up to isomorphism of minimal DFA
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="HereditarilyFinite.shtml">HereditarilyFinite</a></td></tr>
<td class="data"><a href="Regular-Sets.shtml">Regular-Sets</a>, <a href="HereditarilyFinite.shtml">HereditarilyFinite</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -79,6 +79,10 @@ the <a href="http://www.in.tum.de/~nipkow/pubs/itp11/">ITP 2011 paper by Nipkow<
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Trie.shtml">Trie</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -85,7 +85,7 @@ project</a> with it.
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Slicing.shtml">Slicing</a>, <a href="Dijkstra_Shortest_Path.shtml">Dijkstra_Shortest_Path</a></td></tr>
<td class="data"><a href="Slicing.shtml">Slicing</a>, <a href="Collections.shtml">Collections</a>, <a href="Dijkstra_Shortest_Path.shtml">Dijkstra_Shortest_Path</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -81,7 +81,7 @@ Coalgebraic Decision Procedure for WS1S</a> by the author.
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Coinductive_Languages.shtml">Coinductive_Languages</a>, <a href="Deriving.shtml">Deriving</a>, <a href="Show.shtml">Show</a>, <a href="List-Index.shtml">List-Index</a></td></tr>
<td class="data"><a href="Deriving.shtml">Deriving</a>, <a href="Coinductive_Languages.shtml">Coinductive_Languages</a>, <a href="List-Index.shtml">List-Index</a>, <a href="Show.shtml">Show</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -75,10 +75,6 @@ proven, as well as some isomorphisms results about Free Groups.
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Ordinals_and_Cardinals.shtml">Ordinals_and_Cardinals</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -66,6 +66,10 @@ The Gauss-Jordan algorithm states that any matrix over a field can be transforme
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Rank_Nullity_Theorem.shtml">Rank_Nullity_Theorem</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -94,6 +94,10 @@ the underlying algorithmic mechanisms and the kinds of faults they tolerate.
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Stuttering_Equivalence.shtml">Stuttering_Equivalence</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -64,6 +64,10 @@ Hermite Normal Form is a canonical matrix analogue of Reduced Echelon Form, but
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Echelon_Form.shtml">Echelon_Form</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -65,6 +65,10 @@ We introduce Jinja, a Java-like programming language with a formal semantics des
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="List-Index.shtml">List-Index</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -115,7 +115,7 @@ support for non-deterministic memory allocators
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Collections.shtml">Collections</a>, <a href="Coinductive.shtml">Coinductive</a></td></tr>
<td class="data"><a href="Coinductive.shtml">Coinductive</a>, <a href="Collections.shtml">Collections</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -85,7 +85,7 @@ All the results have been applied to improve CeTA, our certifier to validate ter
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Containers.shtml">Containers</a>, <a href="Gauss_Jordan.shtml">Gauss_Jordan</a>, <a href="Matrix.shtml">Matrix</a>, <a href="Abstract-Rewriting.shtml">Abstract-Rewriting</a>, <a href="Show.shtml">Show</a>, <a href="Polynomial_Interpolation.shtml">Polynomial_Interpolation</a>, <a href="VectorSpace.shtml">VectorSpace</a></td></tr>
<td class="data"><a href="Matrix.shtml">Matrix</a>, <a href="Show.shtml">Show</a>, <a href="Gauss_Jordan.shtml">Gauss_Jordan</a>, <a href="Polynomial_Interpolation.shtml">Polynomial_Interpolation</a>, <a href="VectorSpace.shtml">VectorSpace</a>, <a href="Containers.shtml">Containers</a>, <a href="Abstract-Rewriting.shtml">Abstract-Rewriting</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -69,6 +69,10 @@ Knowledge-based programs (KBPs) are a formalism for directly relating agents' kn
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Trie.shtml">Trie</a>, <a href="Transitive-Closure.shtml">Transitive-Closure</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -77,7 +77,7 @@ Recently, Javier Esparza and Jan Kretinsky proposed a new method directly transl
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Boolean_Expression_Checkers.shtml">Boolean_Expression_Checkers</a>, <a href="List-Index.shtml">List-Index</a>, <a href="KBPs.shtml">KBPs</a></td></tr>
<td class="data"><a href="KBPs.shtml">KBPs</a>, <a href="List-Index.shtml">List-Index</a>, <a href="Boolean_Expression_Checkers.shtml">Boolean_Expression_Checkers</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -81,7 +81,7 @@ efficiently executable code can be extracted.
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="CAVA_Automata.shtml">CAVA_Automata</a></td></tr>
<td class="data"><a href="Deriving.shtml">Deriving</a>, <a href="CAVA_Automata.shtml">CAVA_Automata</a>, <a href="Stuttering_Equivalence.shtml">Stuttering_Equivalence</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -73,10 +73,6 @@ intervals.
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Algebraic_Numbers.shtml">Algebraic_Numbers</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -90,6 +90,10 @@ The formalization is described in this <a href="http://www.in.tum.de/~nipkow/pub
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Deriving.shtml">Deriving</a>, <a href="List-Index.shtml">List-Index</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -71,6 +71,10 @@ ZeroConf and an analysis of the anonymity of the Crowds protocol.
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Coinductive.shtml">Coinductive</a>, <a href="Gauss-Jordan-Elim-Fun.shtml">Gauss-Jordan-Elim-Fun</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -66,6 +66,10 @@ Algebras of imperative programming languages have been successful in reasoning a
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="LatticeProperties.shtml">LatticeProperties</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -68,6 +68,10 @@ There are many proofs of the Myhill-Nerode theorem using automata. In this libra
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Well_Quasi_Orders.shtml">Well_Quasi_Orders</a>, <a href="Regular-Sets.shtml">Regular-Sets</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -107,6 +107,10 @@ Added Distributed WebApp example and improved graphviz visualization
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Transitive-Closure.shtml">Transitive-Closure</a>, <a href="Collections.shtml">Collections</a>, <a href="Automatic_Refinement.shtml">Automatic_Refinement</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -65,6 +65,10 @@ A proof of the open induction schema based on J.-C. Raoult, Proving open propert
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Well_Quasi_Orders.shtml">Well_Quasi_Orders</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -70,6 +70,10 @@ We formalize initial value problems (IVPs) of ODEs and prove the existence of a
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Affine_Arithmetic.shtml">Affine_Arithmetic</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -70,7 +70,7 @@ certificates for planarity (i.e., a combinatorial map) or non-planarity
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Simpl.shtml">Simpl</a>, <a href="Case_Labeling.shtml">Case_Labeling</a>, <a href="Graph_Theory.shtml">Graph_Theory</a>, <a href="List-Index.shtml">List-Index</a>, <a href="Transitive-Closure.shtml">Transitive-Closure</a></td></tr>
<td class="data"><a href="Case_Labeling.shtml">Case_Labeling</a>, <a href="Transitive-Closure.shtml">Transitive-Closure</a>, <a href="Graph_Theory.shtml">Graph_Theory</a>, <a href="Simpl.shtml">Simpl</a>, <a href="List-Index.shtml">List-Index</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -78,7 +78,7 @@ as well as primality-testing and prime-factorization algorithms for integers.
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Polynomial_Interpolation.shtml">Polynomial_Interpolation</a>, <a href="Partial_Function_MR.shtml">Partial_Function_MR</a>, <a href="Sqrt_Babylonian.shtml">Sqrt_Babylonian</a>, <a href="Show.shtml">Show</a>, <a href="Jordan_Normal_Form.shtml">Jordan_Normal_Form</a></td></tr>
<td class="data"><a href="Matrix.shtml">Matrix</a>, <a href="Show.shtml">Show</a>, <a href="Sqrt_Babylonian.shtml">Sqrt_Babylonian</a>, <a href="Polynomial_Interpolation.shtml">Polynomial_Interpolation</a>, <a href="Partial_Function_MR.shtml">Partial_Function_MR</a>, <a href="Jordan_Normal_Form.shtml">Jordan_Normal_Form</a>, <a href="Containers.shtml">Containers</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -82,7 +82,7 @@ been essential to formalize polynomial interpretations.
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Abstract-Rewriting.shtml">Abstract-Rewriting</a></td></tr>
<td class="data"><a href="Abstract-Rewriting.shtml">Abstract-Rewriting</a>, <a href="Matrix.shtml">Matrix</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -63,6 +63,10 @@ We formalize a probabilistic noninterference for a multi-threaded language with
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Markov_Models.shtml">Markov_Models</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -74,7 +74,7 @@ system, on which the semantic engine (read: successor function) operates.
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="CAVA_Automata.shtml">CAVA_Automata</a></td></tr>
<td class="data"><a href="Deriving.shtml">Deriving</a>, <a href="CAVA_Automata.shtml">CAVA_Automata</a>, <a href="LTL_to_GBA.shtml">LTL_to_GBA</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -63,6 +63,10 @@ Pseudo-hoops are algebraic structures introduced by B. Bosbach under the name of
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="LatticeProperties.shtml">LatticeProperties</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -69,6 +69,10 @@ QR decomposition is an algorithm to decompose a real matrix A into the product o
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Real_Impl.shtml">Real_Impl</a>, <a href="Rank_Nullity_Theorem.shtml">Rank_Nullity_Theorem</a>, <a href="Gauss_Jordan.shtml">Gauss_Jordan</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -68,6 +68,10 @@ Random graphs are graphs with a fixed number of vertices, where each edge is pre
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Girth_Chromatic.shtml">Girth_Chromatic</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -83,6 +83,10 @@ polynomial interpretations over the reals.
<td class="data"><a href="http://afp.sourceforge.net/LICENSE.LGPL">GNU Lesser General Public License (LGPL)</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Sqrt_Babylonian.shtml">Sqrt_Babylonian</a>, <a href="Show.shtml">Show</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -79,6 +79,10 @@ Interactive Theorem Proving 2014</a>.
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>