2012-03-12 noschinl [Mon, 12 Mar 2012 21:41:11 +0100] rev 46884
tuned proofs
src/HOL/Complete_Lattices.thy src/HOL/Lattices.thy src/HOL/Library/Cset.thy src/HOL/Library/Predicate_Compile_Alternative_Defs.thy src/HOL/List.thy src/HOL/Orderings.thy src/HOL/Predicate.thy src/HOL/Probability/Borel_Space.thy src/HOL/Probability/Lebesgue_Integration.thy src/HOL/Relation.thy

2012-03-12 noschinl [Mon, 12 Mar 2012 15:12:22 +0100] rev 46883
tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
src/HOL/Relation.thy src/HOL/Wellfounded.thy

2012-03-12 noschinl [Mon, 12 Mar 2012 15:11:24 +0100] rev 46882
tuned simpset
src/HOL/Complete_Lattices.thy src/HOL/Lattices.thy src/HOL/Orderings.thy src/HOL/Relation.thy src/HOL/Set.thy src/HOL/Wellfounded.thy

2012-03-12 wenzelm [Mon, 12 Mar 2012 21:31:22 +0100] rev 46881
activate_notes in parallel -- to speedup main operation of locale interpretation;
src/Pure/Isar/locale.ML

2012-03-12 wenzelm [Mon, 12 Mar 2012 20:44:10 +0100] rev 46880
refined activate_notes: simultaneous transformation before activation;
actually export all_registrations_of;
src/Pure/Isar/locale.ML

2012-03-12 wenzelm [Mon, 12 Mar 2012 19:09:38 +0100] rev 46879
tuned headers;
src/HOL/Import/HOL4/Template/GenHOL4Base.thy src/HOL/Import/HOL4/Template/GenHOL4Prob.thy src/HOL/Import/HOL4/Template/GenHOL4Real.thy src/HOL/Import/HOL4/Template/GenHOL4Vec.thy src/HOL/Import/HOL4/Template/GenHOL4Word32.thy src/HOL/Import/HOL_Light/HOLLightInt.thy src/HOL/Import/HOL_Light/HOLLightList.thy src/HOL/Import/HOL_Light/HOLLightReal.thy src/HOL/Import/HOL_Light/Template/GenHOLLight.thy src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML

2012-03-12 paulson [Mon, 12 Mar 2012 16:57:29 +0000] rev 46878
merged

2012-03-12 paulson [Mon, 12 Mar 2012 16:14:25 +0000] rev 46877
Structured proofs in ZF
src/ZF/Cardinal.thy

2012-03-12 wenzelm [Mon, 12 Mar 2012 17:27:52 +0100] rev 46876
refined define_command vs. run_command: static tokenization vs. dynamic parsing, to increase the chance that the proper transaction is run after redefining commands (NB: requires slightly more space and time for document state);
src/Pure/Isar/outer_syntax.ML src/Pure/PIDE/document.ML

2012-03-12 wenzelm [Mon, 12 Mar 2012 16:04:00 +0100] rev 46875
updated polyml/build option to prefer included libffi;
Admin/polyml/build