2011-07-19 hoelzl [Tue, 19 Jul 2011 14:35:44 +0200] rev 43919
rename Nat_Infinity (inat) to Extended_Nat (enat)
src/HOL/HOLCF/FOCUS/Fstreams.thy src/HOL/HOLCF/FOCUS/Stream_adm.thy src/HOL/HOLCF/IsaMakefile src/HOL/HOLCF/Library/Stream.thy src/HOL/IsaMakefile src/HOL/Library/Extended_Nat.thy src/HOL/Library/Library.thy src/HOL/Library/Nat_Infinity.thy

2011-07-20 Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 20 Jul 2011 10:11:08 +0200] rev 43918
HOL/Import reorganization/cleaning. Factor 9 speedup. Remove Import XML parser in favor of much faster of Isabelle's XML parser. Remove ImportRecording since we can use Isabelle images.
src/HOL/Import/HOL4Setup.thy src/HOL/Import/HOLLight/hollight.imp src/HOL/Import/ImportRecorder.thy src/HOL/Import/import_syntax.ML src/HOL/Import/importrecorder.ML src/HOL/Import/lazy_seq.ML src/HOL/Import/mono_scan.ML src/HOL/Import/mono_seq.ML src/HOL/Import/proof_kernel.ML src/HOL/Import/replay.ML src/HOL/Import/scan.ML src/HOL/Import/seq.ML src/HOL/Import/xml.ML src/HOL/Import/xmlconv.ML src/HOL/IsaMakefile

2011-07-20 kleing [Wed, 20 Jul 2011 08:46:17 +0200] rev 43917
build an image for HOL-IMP
src/HOL/IsaMakefile

2011-07-20 bulwahn [Wed, 20 Jul 2011 08:16:42 +0200] rev 43916
deactivating quickcheck invocation in this example until the Interrupt issue is understood
src/HOL/Predicate_Compile_Examples/ROOT.ML

2011-07-20 bulwahn [Wed, 20 Jul 2011 08:16:41 +0200] rev 43915
removing inner time limits in quickcheck
src/HOL/Tools/Quickcheck/narrowing_generators.ML src/Tools/quickcheck.ML

2011-07-20 bulwahn [Wed, 20 Jul 2011 08:16:39 +0200] rev 43914
updating documentation about quickcheck; adding information about try
doc-src/IsarRef/Thy/HOL_Specific.thy doc-src/IsarRef/Thy/document/HOL_Specific.tex

2011-07-20 bulwahn [Wed, 20 Jul 2011 08:16:38 +0200] rev 43913
adapting example in Predicate_Compile_Examples
src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy

2011-07-20 bulwahn [Wed, 20 Jul 2011 08:16:36 +0200] rev 43912
exporting function in quickcheck; adapting mutabelle script
src/HOL/Mutabelle/lib/Tools/mutabelle src/Tools/quickcheck.ML

2011-07-20 bulwahn [Wed, 20 Jul 2011 08:16:35 +0200] rev 43911
more information for the user how to deactivate quickcheck_narrowing if he does not want to use it
src/HOL/Tools/Quickcheck/narrowing_generators.ML

2011-07-20 bulwahn [Wed, 20 Jul 2011 08:16:33 +0200] rev 43910
making messages more informative
src/HOL/Tools/Quickcheck/narrowing_generators.ML