2011-07-19 hoelzl [Tue, 19 Jul 2011 14:37:49 +0200] rev 43922
add nat => enat coercion
src/HOL/Library/Extended_Nat.thy

2011-07-19 hoelzl [Tue, 19 Jul 2011 14:37:09 +0200] rev 43921
Introduce infinity type class
src/HOL/HOLCF/FOCUS/Fstreams.thy src/HOL/HOLCF/FOCUS/Stream_adm.thy src/HOL/HOLCF/Library/Stream.thy src/HOL/Library/Extended_Nat.thy

2011-07-19 hoelzl [Tue, 19 Jul 2011 14:36:12 +0200] rev 43920
Rename extreal => ereal
src/HOL/IsaMakefile src/HOL/Library/Extended_Real.thy src/HOL/Library/Extended_Reals.thy src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy src/HOL/Probability/Binary_Product_Measure.thy src/HOL/Probability/Borel_Space.thy src/HOL/Probability/Caratheodory.thy src/HOL/Probability/Complete_Measure.thy src/HOL/Probability/Conditional_Probability.thy src/HOL/Probability/Finite_Product_Measure.thy src/HOL/Probability/Independent_Family.thy src/HOL/Probability/Infinite_Product_Measure.thy src/HOL/Probability/Information.thy src/HOL/Probability/Lebesgue_Integration.thy src/HOL/Probability/Lebesgue_Measure.thy src/HOL/Probability/Measure.thy src/HOL/Probability/Probability_Measure.thy src/HOL/Probability/Radon_Nikodym.thy src/HOL/Probability/ex/Dining_Cryptographers.thy src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy

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