1.1 --- a/Admin/isatest/isatest-stats	Wed Oct 19 14:22:06 2011 +0200
     1.2 +++ b/Admin/isatest/isatest-stats	Wed Oct 19 14:40:49 2011 +0200
     1.3 @@ -8,161 +8,177 @@
     1.4  
     1.5  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"
     1.6  
     1.7 -ISABELLE_SESSIONS="\
     1.8 -  HOL-Auth \
     1.9 -  HOL-Bali \
    1.10 -  HOL-Boogie-Examples \
    1.11 -  HOL-Decision_Procs \
    1.12 -  HOL-Hahn_Banach \
    1.13 -  HOL-Hoare \
    1.14 -  HOL-Hoare_Parallel \
    1.15 -  HOL-IMPP \
    1.16 -  HOL-IOA \
    1.17 -  HOL-Imperative_HOL \
    1.18 -  HOL-Import \
    1.19 -  HOL-Induct \
    1.20 -  HOL-Isar_Examples \
    1.21 -  HOL-Lattice \
    1.22 -  HOL-Library-Codegenerator_Test \
    1.23 -  HOL-Matrix \
    1.24 -  HOL-Metis_Examples \
    1.25 -  HOL-MicroJava \
    1.26 -  HOL-Mirabelle \
    1.27 -  HOL-Mutabelle \
    1.28 -  HOL-NanoJava \
    1.29 -  HOL-Nitpick_Examples \
    1.30 +ISABELLE_SESSIONS="
    1.31 +  HOL
    1.32 +  HOL-Main
    1.33 +  HOL-Plain
    1.34 +  HOL-Base
    1.35 +  HOL-Library
    1.36 +  HOL-Algebra
    1.37 +  HOL-Auth
    1.38 +  HOL-Bali
    1.39 +  HOL-Boogie
    1.40 +  HOL-Boogie-Examples
    1.41 +  HOL-Decision_Procs
    1.42 +  HOL-Hahn_Banach
    1.43 +  HOL-Hoare
    1.44 +  HOL-Hoare_Parallel
    1.45 +  HOL-IMP
    1.46 +  HOL-IMPP
    1.47 +  HOL-IOA
    1.48 +  HOL-Imperative_HOL
    1.49 +  HOL-Import
    1.50 +  HOL-Induct
    1.51 +  HOL-Isar_Examples
    1.52 +  HOL-Lattice
    1.53 +  HOL-Library-Codegenerator_Test
    1.54 +  HOL-Matrix
    1.55 +  HOL-Metis_Examples
    1.56 +  HOL-MicroJava
    1.57 +  HOL-Mirabelle
    1.58 +  HOL-Multivariate_Analysis
    1.59 +  HOL-Mutabelle
    1.60 +  HOL-NSA
    1.61 +  HOL-NanoJava
    1.62 +  HOL-Nitpick_Examples
    1.63 +  HOL-Nominal
    1.64    HOL-Nominal-Examples
    1.65 -  HOL-Number_Theory \
    1.66 -  HOL-Old_Number_Theory \
    1.67 -  HOL-Predicate_Compile_Examples \
    1.68 +  HOL-Number_Theory
    1.69 +  HOL-Old_Number_Theory
    1.70 +  HOL-Predicate_Compile_Examples
    1.71    HOL-Probability
    1.72 -  HOL-Prolog \
    1.73 -  HOL-Proofs-Extraction \
    1.74 -  HOL-Proofs-Lambda \
    1.75 -  HOL-Proofs-ex \
    1.76 -  HOL-Quotient_Examples \
    1.77 -  HOL-SET_Protocol \
    1.78 -  HOL-SPARK-Examples \
    1.79 -  HOL-SPARK-Manual \
    1.80 -  HOL-Statespace \
    1.81 -  HOL-TPTP \
    1.82 -  HOL-UNITY \
    1.83 -  HOL-Unix \
    1.84 -  HOL-Word-Examples \
    1.85 -  HOL-Word-SMT_Examples \
    1.86 +  HOL-Prolog
    1.87 +  HOL-Proofs
    1.88 +  HOL-Proofs-Extraction
    1.89 +  HOL-Proofs-Lambda
    1.90 +  HOL-Proofs-ex
    1.91 +  HOL-Quotient_Examples
    1.92 +  HOL-SET_Protocol
    1.93 +  HOL-SPARK
    1.94 +  HOL-SPARK-Examples
    1.95 +  HOL-SPARK-Manual
    1.96 +  HOL-Statespace
    1.97 +  HOL-TPTP
    1.98 +  HOL-UNITY
    1.99 +  HOL-Unix
   1.100 +  HOL-Word
   1.101 +  HOL-Word-Examples
   1.102 +  HOL-Word-SMT_Examples
   1.103    HOL-ZF
   1.104 -  HOL-ex \
   1.105 -  HOLCF-FOCUS \
   1.106 -  HOLCF-IMP \
   1.107 -  HOLCF-Library \
   1.108 -  HOLCF-Tutorial \
   1.109 -  HOLCF-ex \
   1.110 -  IOA-ABP \
   1.111 -  IOA-NTP \
   1.112 -  IOA-Storage \
   1.113 -  IOA-ex \
   1.114 -  TLA-Buffer \
   1.115 -  TLA-Inc \
   1.116 +  HOL-ex
   1.117 +  HOL4
   1.118 +  HOLCF
   1.119 +  HOLCF-FOCUS
   1.120 +  HOLCF-IMP
   1.121 +  HOLCF-Library
   1.122 +  HOLCF-Tutorial
   1.123 +  HOLCF-ex
   1.124 +  IOA
   1.125 +  IOA-ABP
   1.126 +  IOA-NTP
   1.127 +  IOA-Storage
   1.128 +  IOA-ex
   1.129 +  TLA
   1.130 +  TLA-Buffer
   1.131 +  TLA-Inc
   1.132    TLA-Memory"
   1.133  
   1.134 -AFP_SESSIONS="\
   1.135 -  ArrowImpossibilityGS \
   1.136 -  Coinductive \
   1.137 -  CoreC++ \
   1.138 -  HOL-AVL-Trees \
   1.139 -  HOL-Abstract-Hoare-Logics \
   1.140 -  HOL-Abstract-Rewriting \
   1.141 -  HOL-BinarySearchTree \
   1.142 -  HOL-Binomial-Heaps \
   1.143 -  HOL-Binomial-Queues \
   1.144 -  HOL-BytecodeLogicJmlTypes \
   1.145 -  HOL-Category \
   1.146 -  HOL-Category2 \
   1.147 -  HOL-Cauchy \
   1.148 -  HOL-ClockSynchInst \
   1.149 -  HOL-CofGroups \
   1.150 -  HOL-Collections \
   1.151 -  HOL-Compiling-Exceptions-Correctly \
   1.152 -  HOL-Completeness \
   1.153 -  HOL-DPT-SAT-Solver \
   1.154 -  HOL-DataRefinementIBP \
   1.155 -  HOL-Depth-First-Search \
   1.156 -  HOL-DiskPaxos \
   1.157 -  HOL-Example-Submission \
   1.158 -  HOL-FFT \
   1.159 -  HOL-FOL-Fitting \
   1.160 -  HOL-FeatherweightJava \
   1.161 -  HOL-FileRefinement \
   1.162 -  HOL-FinFun \
   1.163 -  HOL-Finger-Trees \
   1.164 -  HOL-Flyspeck-Tame \
   1.165 -  HOL-Free-Boolean-Algebra \
   1.166 -  HOL-Free-Groups \
   1.167 -  HOL-FunWithFunctions \
   1.168 -  HOL-FunWithTilings \
   1.169 -  HOL-Functional-Automata \
   1.170 -  HOL-Gauss-Jordan-Elim-Fun \
   1.171 -  HOL-GenClock \
   1.172 -  HOL-General-Triangle \
   1.173 -  HOL-GraphMarkingIBP \
   1.174 -  HOL-HotelKeyCards \
   1.175 -  HOL-Huffman \
   1.176 -  HOL-Integration \
   1.177 -  HOL-JiveDataStoreModel \
   1.178 -  HOL-KBPs \
   1.179 -  HOL-Lazy-Lists-II \
   1.180 -  HOL-LightweightJava \
   1.181 -  HOL-List-Index \
   1.182 -  HOL-Locally-Nameless-Sigma \
   1.183 -  HOL-Marriage \
   1.184 -  HOL-Matrix \
   1.185 -  HOL-Max-Card-Matching \
   1.186 -  HOL-MiniML \
   1.187 -  HOL-MuchAdoAboutTwo \
   1.188 -  HOL-Multivariate_Analysis \
   1.189 -  HOL-Myhill-Nerode \
   1.190 -  HOL-Nominal \
   1.191 -  HOL-Nominal-Lam-ml-Normalization \
   1.192 -  HOL-Nominal-SequentInvertibility \
   1.193 -  HOL-Ordinal \
   1.194 -  HOL-Ordinals_and_Cardinals \
   1.195 -  HOL-POPLmark-deBruijn \
   1.196 -  HOL-Perfect-Number-Thm \
   1.197 -  HOL-Polynomials \
   1.198 -  HOL-Presburger-Automata \
   1.199 -  HOL-Program-Conflict-Analysis \
   1.200 -  HOL-Ramsey-Infinite \
   1.201 -  HOL-Recursion-Theory-I \
   1.202 -  HOL-Regular-Sets \
   1.203 -  HOL-Robbins-Conjecture \
   1.204 -  HOL-SATSolverVerification \
   1.205 -  HOL-SIFPL \
   1.206 -  HOL-SenSocialChoice \
   1.207 -  HOL-Statecharts \
   1.208 -  HOL-Topology \
   1.209 -  HOL-Transitive-Closure \
   1.210 -  HOL-Tree-Automata \
   1.211 -  HOL-Verified-Prover \
   1.212 -  HOL-Word \
   1.213 -  HOL-Word-RIPEMD-160-SPARK \
   1.214 -  HOLCF \
   1.215 -  HOLCF-Shivers-CFA \
   1.216 -  HOLCF-Stream-Fusion \
   1.217 -  HOLCF-WorkerWrapper \
   1.218 -  HRB-Slicing \
   1.219 -  HRB-Slicing-InformationFlowSlicing \
   1.220 -  Jinja \
   1.221 -  Jinja \
   1.222 -  LatticeProperties \
   1.223 -  LatticeProperties-MonoBoolTranAlgebra \
   1.224 -  LatticeProperties-PseudoHoops \
   1.225 -  Lower_Semicontinuous \
   1.226 -  NormByEval \
   1.227 -  Simpl \
   1.228 -  Simpl-BDD \
   1.229 -  Slicing \
   1.230 -  Slicing \
   1.231 -  Slicing-InformationFlowSlicing \
   1.232 +AFP_SESSIONS="
   1.233 +  ArrowImpossibilityGS
   1.234 +  Coinductive
   1.235 +  CoreC++
   1.236 +  HOL-AVL-Trees
   1.237 +  HOL-Abstract-Hoare-Logics
   1.238 +  HOL-Abstract-Rewriting
   1.239 +  HOL-BinarySearchTree
   1.240 +  HOL-Binomial-Heaps
   1.241 +  HOL-Binomial-Queues
   1.242 +  HOL-BytecodeLogicJmlTypes
   1.243 +  HOL-Category
   1.244 +  HOL-Category2
   1.245 +  HOL-Cauchy
   1.246 +  HOL-ClockSynchInst
   1.247 +  HOL-CofGroups
   1.248 +  HOL-Collections
   1.249 +  HOL-Compiling-Exceptions-Correctly
   1.250 +  HOL-Completeness
   1.251 +  HOL-DPT-SAT-Solver
   1.252 +  HOL-DataRefinementIBP
   1.253 +  HOL-Depth-First-Search
   1.254 +  HOL-DiskPaxos
   1.255 +  HOL-Example-Submission
   1.256 +  HOL-FFT
   1.257 +  HOL-FOL-Fitting
   1.258 +  HOL-FeatherweightJava
   1.259 +  HOL-FileRefinement
   1.260 +  HOL-FinFun
   1.261 +  HOL-Finger-Trees
   1.262 +  HOL-Flyspeck-Tame
   1.263 +  HOL-Free-Boolean-Algebra
   1.264 +  HOL-Free-Groups
   1.265 +  HOL-FunWithFunctions
   1.266 +  HOL-FunWithTilings
   1.267 +  HOL-Functional-Automata
   1.268 +  HOL-Gauss-Jordan-Elim-Fun
   1.269 +  HOL-GenClock
   1.270 +  HOL-General-Triangle
   1.271 +  HOL-GraphMarkingIBP
   1.272 +  HOL-HotelKeyCards
   1.273 +  HOL-Huffman
   1.274 +  HOL-Integration
   1.275 +  HOL-JiveDataStoreModel
   1.276 +  HOL-KBPs
   1.277 +  HOL-Lazy-Lists-II
   1.278 +  HOL-LightweightJava
   1.279 +  HOL-List-Index
   1.280 +  HOL-Locally-Nameless-Sigma
   1.281 +  HOL-Marriage
   1.282 +  HOL-Matrix
   1.283 +  HOL-Max-Card-Matching
   1.284 +  HOL-MiniML
   1.285 +  HOL-MuchAdoAboutTwo
   1.286 +  HOL-Multivariate_Analysis
   1.287 +  HOL-Myhill-Nerode
   1.288 +  HOL-Nominal
   1.289 +  HOL-Nominal-Lam-ml-Normalization
   1.290 +  HOL-Nominal-SequentInvertibility
   1.291 +  HOL-Ordinal
   1.292 +  HOL-Ordinals_and_Cardinals
   1.293 +  HOL-POPLmark-deBruijn
   1.294 +  HOL-Perfect-Number-Thm
   1.295 +  HOL-Polynomials
   1.296 +  HOL-Presburger-Automata
   1.297 +  HOL-Program-Conflict-Analysis
   1.298 +  HOL-Ramsey-Infinite
   1.299 +  HOL-Recursion-Theory-I
   1.300 +  HOL-Regular-Sets
   1.301 +  HOL-Robbins-Conjecture
   1.302 +  HOL-SATSolverVerification
   1.303 +  HOL-SIFPL
   1.304 +  HOL-SenSocialChoice
   1.305 +  HOL-Statecharts
   1.306 +  HOL-Topology
   1.307 +  HOL-Transitive-Closure
   1.308 +  HOL-Tree-Automata
   1.309 +  HOL-Verified-Prover
   1.310 +  HOL-Word
   1.311 +  HOL-Word-RIPEMD-160-SPARK
   1.312 +  HOLCF
   1.313 +  HOLCF-Shivers-CFA
   1.314 +  HOLCF-Stream-Fusion
   1.315 +  HOLCF-WorkerWrapper
   1.316 +  HRB-Slicing
   1.317 +  HRB-Slicing-InformationFlowSlicing
   1.318 +  Jinja
   1.319 +  LatticeProperties
   1.320 +  LatticeProperties-MonoBoolTranAlgebra
   1.321 +  LatticeProperties-PseudoHoops
   1.322 +  Lower_Semicontinuous
   1.323 +  NormByEval
   1.324 +  Simpl
   1.325 +  Simpl-BDD
   1.326 +  Slicing
   1.327 +  Slicing-InformationFlowSlicing
   1.328    VolpanoSmith"
   1.329  
   1.330