diff -r c721a0d251b0 -r 37a92211a5d3 Admin/page/main-content/index.content --- a/Admin/page/main-content/index.content Fri Apr 16 04:06:25 2004 +0200 +++ b/Admin/page/main-content/index.content Fri Apr 16 04:06:52 2004 +0200 @@ -35,6 +35,44 @@
+
+New features in include +ring
for non-commutative rings in HOL-Algebra.rat
of the rational numbers available in HOL-Complex.specification
command for definition by specification.finalconsts
prevents constants being given a definition later.arith
now generates counterexamples for reals as well.refute
command to search for (finite) countermodels for a fragment of HOL.+The distribution is available +from several mirror sites. It includes +source and binary packages and browsable documentation. There is also +a nightly generated development +snapshot available. + +
+
-
- You can also browse the Isabelle theory library; the main logics are HOL,