Start test at Mon Sep  1 08:31:21 CEST 2008, atbroy51

begin cvs update
? thys/ClockSynchInst/document/abs_distrib_mult.cvc
? thys/ClockSynchInst/document/abs_distrib_mult.ics
? thys/ClockSynchInst/document/abs_distrib_mult2.cvc
? thys/ClockSynchInst/document/accur_pres.cvc
? thys/ClockSynchInst/document/accur_pres.ics
? thys/ClockSynchInst/document/bound_prec_enh.cvc
? thys/ClockSynchInst/document/bound_prec_enh.ics
? thys/ClockSynchInst/document/bound_prec_enh4.cvc
? thys/ClockSynchInst/document/bound_prec_enh7.cvc
? thys/JinjaThreads/generated
end cvs update

Testing [AVL-Trees]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL AVL-Trees
Running HOL-AVL-Trees ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/AVL-Trees
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/AVL-Trees/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/AVL-Trees/outline.pdf
Finished HOL-AVL-Trees (0:01:03 elapsed time, 0:00:32 cpu time)
Finished [AVL-Trees]
Testing [Abstract-Hoare-Logics]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL Abstract-Hoare-Logics
Running HOL-Abstract-Hoare-Logics ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Abstract-Hoare-Logics
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Abstract-Hoare-Logics/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Abstract-Hoare-Logics/outline.pdf
Finished HOL-Abstract-Hoare-Logics (0:00:42 elapsed time, 0:00:37 cpu time)
Finished [Abstract-Hoare-Logics]
Testing [BDD]
cd ../Simpl; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool make Simpl 
make[1]: Entering directory `/mnt/home/isatest/afp/devel/thys/Simpl'
ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -g true -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  -b /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL Simpl
Building Simpl ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Simpl
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Simpl/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Simpl/outline.pdf
Finished Simpl (0:07:47 elapsed time, 0:07:07 cpu time)
make[1]: Leaving directory `/mnt/home/isatest/afp/devel/thys/Simpl'
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -g true -i true -V outline=/proof,/ML -d pdf  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/Simpl BDD
Running Simpl-BDD ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Simpl/BDD
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Simpl/BDD/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Simpl/BDD/outline.pdf
Finished Simpl-BDD (0:03:34 elapsed time, 0:03:11 cpu time)
Finished [BDD]
Testing [BinarySearchTree]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL BinarySearchTree
Running HOL-BinarySearchTree ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/BinarySearchTree
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/BinarySearchTree/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/BinarySearchTree/outline.pdf
Finished HOL-BinarySearchTree (0:00:31 elapsed time, 0:00:09 cpu time)
Finished [BinarySearchTree]
Testing [Category]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL Category
Running HOL-Category ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Category
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Category/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Category/outline.pdf
Finished HOL-Category (0:00:25 elapsed time, 0:00:10 cpu time)
Finished [Category]
Testing [Cauchy]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL Cauchy
Running HOL-Cauchy ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Cauchy
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Cauchy/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Cauchy/outline.pdf
Finished HOL-Cauchy (0:00:16 elapsed time, 0:00:10 cpu time)
Finished [Cauchy]
Testing [ClockSynchInst]
cp -f abs_distrib_mult.ics abs_distrib_mult.cvc abs_distrib_mult2.cvc bound_prec_enh4.cvc bound_prec_enh.cvc bound_prec_enh7.cvc bound_prec_enh.ics accur_pres.cvc accur_pres.ics document/
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL ClockSynchInst
Running HOL-ClockSynchInst ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/ClockSynchInst
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/ClockSynchInst/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/ClockSynchInst/outline.pdf
Finished HOL-ClockSynchInst (0:00:22 elapsed time, 0:00:15 cpu time)
Finished [ClockSynchInst]
Testing [Compiling-Exceptions-Correctly]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL Compiling-Exceptions-Correctly
Running HOL-Compiling-Exceptions-Correctly ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Compiling-Exceptions-Correctly
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Compiling-Exceptions-Correctly/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Compiling-Exceptions-Correctly/outline.pdf
Finished HOL-Compiling-Exceptions-Correctly (0:00:14 elapsed time, 0:00:06 cpu time)
Finished [Compiling-Exceptions-Correctly]
Testing [Completeness]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL Completeness
Running HOL-Completeness ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Completeness
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Completeness/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Completeness/outline.pdf
Finished HOL-Completeness (0:00:36 elapsed time, 0:00:31 cpu time)
Finished [Completeness]
Testing [CoreC++]
ulimit -t 2000; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -b -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL CoreC++
Building CoreC++ ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/CoreC++
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/CoreC++/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/CoreC++/outline.pdf
Finished CoreC++ (0:08:46 elapsed time, 0:08:00 cpu time)
Finished [CoreC++]
Testing [Depth-First-Search]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL Depth-First-Search
Running HOL-Depth-First-Search ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Depth-First-Search
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Depth-First-Search/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Depth-First-Search/outline.pdf
Finished HOL-Depth-First-Search (0:00:08 elapsed time, 0:00:05 cpu time)
Finished [Depth-First-Search]
Testing [DiskPaxos]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL DiskPaxos
Running HOL-DiskPaxos ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/DiskPaxos
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/DiskPaxos/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/DiskPaxos/outline.pdf
Finished HOL-DiskPaxos (0:01:37 elapsed time, 0:01:29 cpu time)
Finished [DiskPaxos]
Testing [Example-Submission]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL Example-Submission
Running HOL-Example-Submission ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Example-Submission
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Example-Submission/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Example-Submission/outline.pdf
Finished HOL-Example-Submission (0:00:04 elapsed time, 0:00:01 cpu time)
Finished [Example-Submission]
Testing [FFT]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL FFT
Running HOL-FFT ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/FFT
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/FFT/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/FFT/outline.pdf
Finished HOL-FFT (0:00:09 elapsed time, 0:00:06 cpu time)
Finished [FFT]
Testing [FOL-Fitting]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL FOL-Fitting
Running HOL-FOL-Fitting ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/FOL-Fitting
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/FOL-Fitting/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/FOL-Fitting/outline.pdf
Finished HOL-FOL-Fitting (0:00:35 elapsed time, 0:00:29 cpu time)
Finished [FOL-Fitting]
Testing [FeatherweightJava]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL FeatherweightJava
Running HOL-FeatherweightJava ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/FeatherweightJava
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/FeatherweightJava/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/FeatherweightJava/outline.pdf
Finished HOL-FeatherweightJava (0:00:30 elapsed time, 0:00:24 cpu time)
Finished [FeatherweightJava]
Testing [Fermat3_4]
cd ..; ulimit -t 600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL Fermat3_4
Running HOL-Fermat3_4 ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Fermat3_4
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Fermat3_4/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Fermat3_4/outline.pdf
Finished HOL-Fermat3_4 (0:02:09 elapsed time, 0:02:02 cpu time)
Finished [Fermat3_4]
Testing [FileRefinement]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL FileRefinement
Running HOL-FileRefinement ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/FileRefinement
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/FileRefinement/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/FileRefinement/outline.pdf
Finished HOL-FileRefinement (0:00:19 elapsed time, 0:00:15 cpu time)
Finished [FileRefinement]
Testing [Flyspeck-Tame]
cd ..; ulimit -t 20000; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL Flyspeck-Tame
Running HOL-Flyspeck-Tame ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Flyspeck-Tame
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Flyspeck-Tame/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Flyspeck-Tame/outline.pdf
Finished HOL-Flyspeck-Tame (1:44:28 elapsed time, 1:44:03 cpu time)
Finished [Flyspeck-Tame]
Testing [FunWithFunctions]
cd ..; ulimit -t 100; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL FunWithFunctions
Running HOL-FunWithFunctions ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/FunWithFunctions
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/FunWithFunctions/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/FunWithFunctions/outline.pdf
Finished HOL-FunWithFunctions (0:00:09 elapsed time, 0:00:04 cpu time)
Finished [FunWithFunctions]
Testing [Functional-Automata]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL Functional-Automata
Running HOL-Functional-Automata ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Functional-Automata
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Functional-Automata/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Functional-Automata/outline.pdf
Finished HOL-Functional-Automata (0:00:37 elapsed time, 0:00:31 cpu time)
Finished [Functional-Automata]
Testing [GenClock]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL GenClock
Running HOL-GenClock ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/GenClock
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/GenClock/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/GenClock/outline.pdf
Finished HOL-GenClock (0:00:17 elapsed time, 0:00:12 cpu time)
Finished [GenClock]
Testing [Group-Ring-Module]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL Group-Ring-Module
Running HOL-Group-Ring-Module ...
Warning: missing document directory
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Group-Ring-Module
Finished HOL-Group-Ring-Module (0:10:10 elapsed time, 0:09:59 cpu time)
Finished [Group-Ring-Module]
Testing [HotelKeyCards]
cd ..; ulimit -t 600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL HotelKeyCards
Running HOL-HotelKeyCards ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/HotelKeyCards
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/HotelKeyCards/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/HotelKeyCards/outline.pdf
Finished HOL-HotelKeyCards (0:00:25 elapsed time, 0:00:18 cpu time)
Finished [HotelKeyCards]
Testing [Integration]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL-NSA Integration
Running HOL-NSA-Integration ...
HOL-NSA-Integration FAILED
(see also /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/log/HOL-NSA-Integration)

### ("Trueprop"
###   ("op =" "\<^const>Rational.field_char_0_class.Rats"
###     ("_applC" range n_to_rat)))
*** Ambiguous input, 2 terms are type correct:
*** (\<rat> = (range n_to_rat))
*** (Rats = (range n_to_rat))
*** Failed to parse proposition (line 53 of "/mnt/home/isatest/afp/devel/thys/Integration/Rats.thy")
*** At command "definition" (line 51 of "/mnt/home/isatest/afp/devel/thys/Integration/Rats.thy").
Exception- TOPLEVEL_ERROR raised
*** exception Fail raised: ML error

make: *** [/home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/log/HOL-NSA-Integration.gz] Error 1
Finished [Integration]
Testing [Jinja]
cd ..; ulimit -t 5400; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -g true -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL Jinja
Running HOL-Jinja ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Jinja
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Jinja/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Jinja/outline.pdf
Finished HOL-Jinja (0:18:23 elapsed time, 0:18:03 cpu time)
Finished [Jinja]
Testing [JinjaThreads]
cd ..; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -g true -d pdf -P "http://isabelle.in.tum.de/library/" -D generated /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL JinjaThreads
Running HOL-JinjaThreads ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/JinjaThreads
Document sources at /mnt/home/isatest/afp/devel/thys/JinjaThreads/generated
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/JinjaThreads/document.pdf
Finished HOL-JinjaThreads (0:14:53 elapsed time, 0:14:38 cpu time)
Finished [JinjaThreads]
Testing [JiveDataStoreModel]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -g true -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL JiveDataStoreModel
Running HOL-JiveDataStoreModel ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/JiveDataStoreModel
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/JiveDataStoreModel/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/JiveDataStoreModel/outline.pdf
Finished HOL-JiveDataStoreModel (0:02:28 elapsed time, 0:02:15 cpu time)
Finished [JiveDataStoreModel]
Testing [Lazy-Lists-II]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL Lazy-Lists-II
Running HOL-Lazy-Lists-II ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Lazy-Lists-II
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Lazy-Lists-II/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Lazy-Lists-II/outline.pdf
Finished HOL-Lazy-Lists-II (0:00:22 elapsed time, 0:00:17 cpu time)
Finished [Lazy-Lists-II]
Testing [LinearQuantifierElim]
ulimit -t 600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" -b /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL LinearQuantifierElim
Building LinearQuantifierElim ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/LinearQuantifierElim
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/LinearQuantifierElim/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/LinearQuantifierElim/outline.pdf
Finished LinearQuantifierElim (0:06:08 elapsed time, 0:05:15 cpu time)
Finished [LinearQuantifierElim]
Testing [MiniML]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL MiniML
Running HOL-MiniML ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/MiniML
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/MiniML/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/MiniML/outline.pdf
Finished HOL-MiniML (0:00:32 elapsed time, 0:00:27 cpu time)
Finished [MiniML]
Testing [MuchAdoAboutTwo]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL MuchAdoAboutTwo
Running HOL-MuchAdoAboutTwo ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/MuchAdoAboutTwo
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/MuchAdoAboutTwo/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/MuchAdoAboutTwo/outline.pdf
Finished HOL-MuchAdoAboutTwo (0:00:29 elapsed time, 0:00:23 cpu time)
Finished [MuchAdoAboutTwo]
Testing [NormByEval]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL NormByEval
Running HOL-NormByEval ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/NormByEval
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/NormByEval/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/NormByEval/outline.pdf
Finished HOL-NormByEval (0:00:34 elapsed time, 0:00:30 cpu time)
Finished [NormByEval]
Testing [Ordinal]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL Ordinal
Running HOL-Ordinal ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Ordinal
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Ordinal/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Ordinal/outline.pdf
Finished HOL-Ordinal (0:00:20 elapsed time, 0:00:15 cpu time)
Finished [Ordinal]
Testing [POPLmark-deBruijn]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL POPLmark-deBruijn
Running HOL-POPLmark-deBruijn ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/POPLmark-deBruijn
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/POPLmark-deBruijn/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/POPLmark-deBruijn/outline.pdf
Finished HOL-POPLmark-deBruijn (0:01:09 elapsed time, 0:01:03 cpu time)
Finished [POPLmark-deBruijn]
Testing [Program-Conflict-Analysis]
cd ..; ulimit -t 600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL Program-Conflict-Analysis
Running HOL-Program-Conflict-Analysis ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Program-Conflict-Analysis
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Program-Conflict-Analysis/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Program-Conflict-Analysis/outline.pdf
Finished HOL-Program-Conflict-Analysis (0:01:57 elapsed time, 0:01:50 cpu time)
Finished [Program-Conflict-Analysis]
Testing [RSAPSS]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL RSAPSS
Running HOL-RSAPSS ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/RSAPSS
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/RSAPSS/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/RSAPSS/outline.pdf
Finished HOL-RSAPSS (0:01:18 elapsed time, 0:01:12 cpu time)
Finished [RSAPSS]
Testing [Ramsey-Infinite]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL Ramsey-Infinite
Running HOL-Ramsey-Infinite ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Ramsey-Infinite
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Ramsey-Infinite/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Ramsey-Infinite/outline.pdf
Finished HOL-Ramsey-Infinite (0:00:16 elapsed time, 0:00:12 cpu time)
Finished [Ramsey-Infinite]
Testing [Recursion-Theory-I]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  HOL Recursion-Theory-I
Running HOL-Recursion-Theory-I ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Recursion-Theory-I
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Recursion-Theory-I/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Recursion-Theory-I/outline.pdf
Finished HOL-Recursion-Theory-I (0:01:17 elapsed time, 0:01:11 cpu time)
Finished [Recursion-Theory-I]
Testing [SATSolverVerification]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL SATSolverVerification
Running HOL-SATSolverVerification ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/SATSolverVerification
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/SATSolverVerification/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/SATSolverVerification/outline.pdf
Finished HOL-SATSolverVerification (0:01:30 elapsed time, 0:00:56 cpu time)
Finished [SATSolverVerification]
Testing [Simpl]
make: Nothing to be done for `all'.
Finished [Simpl]
Testing [SumSquares]
cd ..; ulimit -t 600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL SumSquares
Running HOL-SumSquares ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/SumSquares
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/SumSquares/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/SumSquares/outline.pdf
Finished HOL-SumSquares (0:01:42 elapsed time, 0:01:31 cpu time)
Finished [SumSquares]
Testing [Topology]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL Topology
Running HOL-Topology ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Topology
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Topology/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Topology/outline.pdf
Finished HOL-Topology (0:01:07 elapsed time, 0:00:53 cpu time)
Finished [Topology]
Testing [Valuation]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL Valuation
Running HOL-Valuation ...
Warning: missing document directory
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Valuation
Finished HOL-Valuation (0:12:18 elapsed time, 0:12:10 cpu time)
Finished [Valuation]
Testing [Verified-Prover]
cd ..; ulimit -t 3600; /mnt/tmp/isatest/isadist/Isabelle_01-Sep-2008/bin/isatool usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"  /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/HOL Verified-Prover
Running HOL-Verified-Prover ...
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Verified-Prover
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Verified-Prover/document.pdf
Document at /home/isatest/isabelle-at-poly/browser_info/HOL-Plain/HOL/Verified-Prover/outline.pdf
Finished HOL-Verified-Prover (0:00:26 elapsed time, 0:00:20 cpu time)
Finished [Verified-Prover]
The following tests failed:
Integration 
Please check logs.

End test on Mon Sep  1 12:07:05 CEST 2008, atbroy51, elapsed time: 3:36:04

