# HG changeset patch
# User wenzelm
# Date 1158695349 -7200
# Node ID 8f2731bfe86f7b796476cbb534fb48fbd34496b2
# Parent  706c22b3a8fb1a60248ae0cdda0f474fc0fefe34
Standard statistics.

diff -r 706c22b3a8fb -r 8f2731bfe86f Admin/isatest-stats
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest-stats	Tue Sep 19 21:49:09 2006 +0200
@@ -0,0 +1,26 @@
+#!/usr/bin/env bash
+#
+# $Id$
+# Author: Makarius
+#
+# DESCRIPTION: Standard statistics.
+
+THIS=$(cd "$(dirname "$0")"; pwd -P)
+
+"$THIS/isatest-statistics" stats/at-poly at-poly 100 \
+  HOL \
+  HOL-Algebra \
+  HOL-Auth \
+  HOL-Bali \
+  HOL-Complex \
+  HOL-Extraction \
+  HOL-Hoare \
+  HOL-HoareParallel \
+  HOL-Lambda \
+  HOL-MicroJava \
+  HOL-NumberTheory \
+  HOL-SET-Protocol \
+  HOL-UNITY \
+  HOL-ex \
+  ZF \
+  ZF-Constructible