more complete stats, including small sessions which provide some clues on main HOL baseline performance;

--- a/Admin/isatest/isatest-stats	Thu Oct 13 23:35:15 2011 +0200
+++ b/Admin/isatest/isatest-stats	Fri Oct 14 11:34:30 2011 +0200
@@ -9,76 +9,162 @@
 PLATFORMS="at-poly at-poly-test afp at64-poly cygwin-poly-e mac-poly-M2 mac-poly-M4 mac-poly64-M2 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at64-poly-5.1-para at-mac-poly-5.1-para at-sml-dev"
 
 ISABELLE_SESSIONS="\
-  HOL-Plain \
-  HOL-Main \
-  HOL \
-  HOL-Proofs \
-  HOL-Library \
-  HOL-Algebra \
   HOL-Auth \
   HOL-Bali \
+  HOL-Boogie-Examples \
   HOL-Decision_Procs \
+  HOL-Hahn_Banach \
   HOL-Hoare \
   HOL-Hoare_Parallel \
+  HOL-IMPP \
+  HOL-IOA \
   HOL-Imperative_HOL \
+  HOL-Import \
+  HOL-Induct \
+  HOL-Isar_Examples \
+  HOL-Lattice \
+  HOL-Library-Codegenerator_Test \
+  HOL-Matrix \
   HOL-Metis_Examples \
   HOL-MicroJava \
-  HOL-Multivariate_Analysis \
-  HOL-NSA \
-  HOL-Nominal-Examples \
+  HOL-Mirabelle \
+  HOL-Mutabelle \
+  HOL-NanoJava \
+  HOL-Nitpick_Examples \
+  HOL-Nominal-Examples
   HOL-Number_Theory \
   HOL-Old_Number_Theory \
   HOL-Predicate_Compile_Examples \
+  HOL-Probability
+  HOL-Prolog \
   HOL-Proofs-Extraction \
   HOL-Proofs-Lambda \
+  HOL-Proofs-ex \
+  HOL-Quotient_Examples \
   HOL-SET_Protocol \
+  HOL-SPARK-Examples \
+  HOL-SPARK-Manual \
+  HOL-Statespace \
+  HOL-TPTP \
   HOL-UNITY \
-  HOL-Word \
+  HOL-Unix \
+  HOL-Word-Examples \
   HOL-Word-SMT_Examples \
+  HOL-ZF
   HOL-ex \
-  HOLCF \
-  IOA \
-  ZF \
-  ZF-Constructible \
-  ZF-UNITY"
+  HOLCF-FOCUS \
+  HOLCF-IMP \
+  HOLCF-Library \
+  HOLCF-Tutorial \
+  HOLCF-ex \
+  IOA-ABP \
+  IOA-NTP \
+  IOA-Storage \
+  IOA-ex \
+  TLA-Buffer \
+  TLA-Inc \
+  TLA-Memory"
 
 AFP_SESSIONS="\
+  ArrowImpossibilityGS \
   Coinductive \
   CoreC++ \
-  Group-Ring-Module \
-  Group-Ring-Module-Valuation \
+  HOL-AVL-Trees \
+  HOL-Abstract-Hoare-Logics \
+  HOL-Abstract-Rewriting \
+  HOL-BinarySearchTree \
+  HOL-Binomial-Heaps \
+  HOL-Binomial-Queues \
   HOL-BytecodeLogicJmlTypes \
+  HOL-Category \
+  HOL-Category2 \
+  HOL-Cauchy \
+  HOL-ClockSynchInst \
+  HOL-CofGroups \
   HOL-Collections \
+  HOL-Compiling-Exceptions-Correctly \
+  HOL-Completeness \
+  HOL-DPT-SAT-Solver \
+  HOL-DataRefinementIBP \
+  HOL-Depth-First-Search \
   HOL-DiskPaxos \
+  HOL-Example-Submission \
+  HOL-FFT \
+  HOL-FOL-Fitting \
   HOL-FeatherweightJava \
-  HOL-Fermat3_4 \
+  HOL-FileRefinement \
+  HOL-FinFun \
+  HOL-Finger-Trees \
   HOL-Flyspeck-Tame \
+  HOL-Free-Boolean-Algebra \
   HOL-Free-Groups \
+  HOL-FunWithFunctions \
+  HOL-FunWithTilings \
+  HOL-Functional-Automata \
+  HOL-Gauss-Jordan-Elim-Fun \
+  HOL-GenClock \
+  HOL-General-Triangle \
   HOL-GraphMarkingIBP \
+  HOL-HotelKeyCards \
+  HOL-Huffman \
+  HOL-Integration \
   HOL-JiveDataStoreModel \
+  HOL-KBPs \
+  HOL-Lazy-Lists-II \
+  HOL-LightweightJava \
+  HOL-List-Index \
   HOL-Locally-Nameless-Sigma \
+  HOL-Marriage \
+  HOL-Matrix \
+  HOL-Max-Card-Matching \
+  HOL-MiniML \
+  HOL-MuchAdoAboutTwo \
+  HOL-Multivariate_Analysis \
+  HOL-Myhill-Nerode \
+  HOL-Nominal \
+  HOL-Nominal-Lam-ml-Normalization \
+  HOL-Nominal-SequentInvertibility \
+  HOL-Ordinal \
   HOL-Ordinals_and_Cardinals \
   HOL-POPLmark-deBruijn \
+  HOL-Perfect-Number-Thm \
+  HOL-Polynomials \
   HOL-Presburger-Automata \
   HOL-Program-Conflict-Analysis \
-  HOL-RSAPSS \
+  HOL-Ramsey-Infinite \
   HOL-Recursion-Theory-I \
+  HOL-Regular-Sets \
+  HOL-Robbins-Conjecture \
   HOL-SATSolverVerification \
   HOL-SIFPL \
   HOL-SenSocialChoice \
-  HOL-SumSquares \
+  HOL-Statecharts \
   HOL-Topology \
+  HOL-Transitive-Closure \
   HOL-Tree-Automata \
-  HOL-Word-JinjaThreads \
+  HOL-Verified-Prover \
+  HOL-Word \
+  HOL-Word-RIPEMD-160-SPARK \
+  HOLCF \
+  HOLCF-Shivers-CFA \
+  HOLCF-Stream-Fusion \
   HOLCF-WorkerWrapper \
   HRB-Slicing \
+  HRB-Slicing-InformationFlowSlicing \
   Jinja \
-  Jinja-Slicing \
-  LinearQuantifierElim \
+  Jinja \
+  LatticeProperties \
+  LatticeProperties-MonoBoolTranAlgebra \
+  LatticeProperties-PseudoHoops \
+  Lower_Semicontinuous \
+  NormByEval \
   Simpl \
   Simpl-BDD \
   Slicing \
-  Slicing-InformationFlowSlicing"
+  Slicing \
+  Slicing-InformationFlowSlicing \
+  VolpanoSmith"
+
 
 for PLATFORM in $PLATFORMS
 do