Commit 400eb684 authored by nipkow's avatar nipkow
Browse files

tuned html

parent 84f44ec186c7
......@@ -520,7 +520,7 @@ abstract =
datastructures---like balanced trees---demands that the type of keys is
linearly ordered.
<p>
Our formalization was performed as part of the \isafor/\ceta{} project.
Our formalization was performed as part of the <a href="http://cl-informatik.uibk.ac.at/software/ceta">IsaFoR/CeTA</a> project.
With our new tactic we could completely remove
tedious proofs for linear orders of two datatypes.
......
......@@ -53,7 +53,7 @@ Our method complements the Isabelle Collection Framework which for some
datastructures---like balanced trees---demands that the type of keys is
linearly ordered.
<p>
Our formalization was performed as part of the \isafor/\ceta{} project.
Our formalization was performed as part of the <a href="http://cl-informatik.uibk.ac.at/software/ceta">IsaFoR/CeTA</a> project.
With our new tactic we could completely remove
tedious proofs for linear orders of two datatypes.
</td></tr>
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment