# HG changeset patch
# User wenzelm
# Date 1319028049 -7200
# Node ID d825a8f1d08884b5f109fd8cfda2884aa6933c6b
# Parent  3181c64be1b4b072415057428ed067d731d34b0e
further cleanup of stats (cf. 97e81a8aa277);

diff -r 3181c64be1b4 -r d825a8f1d088 Admin/isatest/isatest-stats
--- a/Admin/isatest/isatest-stats	Wed Oct 19 14:22:06 2011 +0200
+++ b/Admin/isatest/isatest-stats	Wed Oct 19 14:40:49 2011 +0200
@@ -8,161 +8,177 @@
 
 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-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-Mirabelle \
-  HOL-Mutabelle \
-  HOL-NanoJava \
-  HOL-Nitpick_Examples \
+ISABELLE_SESSIONS="
+  HOL
+  HOL-Main
+  HOL-Plain
+  HOL-Base
+  HOL-Library
+  HOL-Algebra
+  HOL-Auth
+  HOL-Bali
+  HOL-Boogie
+  HOL-Boogie-Examples
+  HOL-Decision_Procs
+  HOL-Hahn_Banach
+  HOL-Hoare
+  HOL-Hoare_Parallel
+  HOL-IMP
+  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-Mirabelle
+  HOL-Multivariate_Analysis
+  HOL-Mutabelle
+  HOL-NSA
+  HOL-NanoJava
+  HOL-Nitpick_Examples
+  HOL-Nominal
   HOL-Nominal-Examples
-  HOL-Number_Theory \
-  HOL-Old_Number_Theory \
-  HOL-Predicate_Compile_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-Unix \
-  HOL-Word-Examples \
-  HOL-Word-SMT_Examples \
+  HOL-Prolog
+  HOL-Proofs
+  HOL-Proofs-Extraction
+  HOL-Proofs-Lambda
+  HOL-Proofs-ex
+  HOL-Quotient_Examples
+  HOL-SET_Protocol
+  HOL-SPARK
+  HOL-SPARK-Examples
+  HOL-SPARK-Manual
+  HOL-Statespace
+  HOL-TPTP
+  HOL-UNITY
+  HOL-Unix
+  HOL-Word
+  HOL-Word-Examples
+  HOL-Word-SMT_Examples
   HOL-ZF
-  HOL-ex \
-  HOLCF-FOCUS \
-  HOLCF-IMP \
-  HOLCF-Library \
-  HOLCF-Tutorial \
-  HOLCF-ex \
-  IOA-ABP \
-  IOA-NTP \
-  IOA-Storage \
-  IOA-ex \
-  TLA-Buffer \
-  TLA-Inc \
+  HOL-ex
+  HOL4
+  HOLCF
+  HOLCF-FOCUS
+  HOLCF-IMP
+  HOLCF-Library
+  HOLCF-Tutorial
+  HOLCF-ex
+  IOA
+  IOA-ABP
+  IOA-NTP
+  IOA-Storage
+  IOA-ex
+  TLA
+  TLA-Buffer
+  TLA-Inc
   TLA-Memory"
 
-AFP_SESSIONS="\
-  ArrowImpossibilityGS \
-  Coinductive \
-  CoreC++ \
-  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-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-Ramsey-Infinite \
-  HOL-Recursion-Theory-I \
-  HOL-Regular-Sets \
-  HOL-Robbins-Conjecture \
-  HOL-SATSolverVerification \
-  HOL-SIFPL \
-  HOL-SenSocialChoice \
-  HOL-Statecharts \
-  HOL-Topology \
-  HOL-Transitive-Closure \
-  HOL-Tree-Automata \
-  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 \
-  LatticeProperties \
-  LatticeProperties-MonoBoolTranAlgebra \
-  LatticeProperties-PseudoHoops \
-  Lower_Semicontinuous \
-  NormByEval \
-  Simpl \
-  Simpl-BDD \
-  Slicing \
-  Slicing \
-  Slicing-InformationFlowSlicing \
+AFP_SESSIONS="
+  ArrowImpossibilityGS
+  Coinductive
+  CoreC++
+  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-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-Ramsey-Infinite
+  HOL-Recursion-Theory-I
+  HOL-Regular-Sets
+  HOL-Robbins-Conjecture
+  HOL-SATSolverVerification
+  HOL-SIFPL
+  HOL-SenSocialChoice
+  HOL-Statecharts
+  HOL-Topology
+  HOL-Transitive-Closure
+  HOL-Tree-Automata
+  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
+  LatticeProperties
+  LatticeProperties-MonoBoolTranAlgebra
+  LatticeProperties-PseudoHoops
+  Lower_Semicontinuous
+  NormByEval
+  Simpl
+  Simpl-BDD
+  Slicing
+  Slicing-InformationFlowSlicing
   VolpanoSmith"