2010-10-07 huffman [Thu, 07 Oct 2010 13:18:48 -0700] rev 39981
remove some junk that made it in by accient
src/HOLCF/CompactBasis.thy

2010-10-11 blanchet [Mon, 11 Oct 2010 18:03:47 +0700] rev 39980
"setup" in theory
src/HOL/Metis.thy

2010-10-11 blanchet [Mon, 11 Oct 2010 18:03:18 +0700] rev 39979
added "trace_meson" configuration option, replacing old-fashioned reference
src/HOL/Tools/Meson/meson.ML src/HOL/Tools/Metis/metis_tactics.ML

2010-10-11 blanchet [Mon, 11 Oct 2010 18:02:14 +0700] rev 39978
added "trace_metis" configuration option, replacing old-fashioned references
src/HOL/Tools/Metis/metis_reconstruct.ML src/HOL/Tools/Metis/metis_tactics.ML

2010-10-10 krauss [Sun, 10 Oct 2010 23:16:24 +0200] rev 39977
do not mention unqualified names, now that 'global' and 'local' are gone
doc-src/IsarRef/Thy/Spec.thy doc-src/IsarRef/Thy/document/Spec.tex

2010-10-10 nipkow [Sun, 10 Oct 2010 16:34:20 +0200] rev 39976
simplified proof
src/HOL/MicroJava/Comp/AuxLemmas.thy

2010-10-10 blanchet [Sun, 10 Oct 2010 18:42:13 +0700] rev 39975
avoid generating several formulas with the same name ("tfrees")
src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML

2010-10-06 huffman [Wed, 06 Oct 2010 10:49:27 -0700] rev 39974
major reorganization/simplification of HOLCF type classes:
removed profinite/bifinite classes and approx function;
universal domain uses approx_chain locale instead of bifinite class;
ideal_completion locale does not use 'take' functions, requires countable basis instead;
replaced type 'udom alg_defl' with type 'sfp';
replaced class 'rep' with class 'sfp';
renamed REP('a) to SFP('a);
src/HOLCF/Algebraic.thy src/HOLCF/Bifinite.thy src/HOLCF/CompactBasis.thy src/HOLCF/Completion.thy src/HOLCF/ConvexPD.thy src/HOLCF/Cprod.thy src/HOLCF/Eventual.thy src/HOLCF/HOLCF.thy src/HOLCF/IsaMakefile src/HOLCF/Library/Strict_Fun.thy src/HOLCF/Library/Sum_Cpo.thy src/HOLCF/Lift.thy src/HOLCF/LowerPD.thy src/HOLCF/Powerdomains.thy src/HOLCF/Representable.thy src/HOLCF/Sprod.thy src/HOLCF/Ssum.thy src/HOLCF/Tools/Domain/domain_extender.ML src/HOLCF/Tools/Domain/domain_isomorphism.ML src/HOLCF/Tools/repdef.ML src/HOLCF/Tutorial/New_Domain.thy src/HOLCF/Universal.thy src/HOLCF/Up.thy src/HOLCF/UpperPD.thy src/HOLCF/ex/Domain_Proofs.thy src/HOLCF/ex/Powerdomain_ex.thy

2010-10-05 Brian Huffman <brianh@cs.pdx.edu> [Tue, 05 Oct 2010 17:53:00 -0700] rev 39973
add lemma finite_deflation_intro
src/HOLCF/Bifinite.thy src/HOLCF/Deflation.thy src/HOLCF/Powerdomains.thy src/HOLCF/Sprod.thy src/HOLCF/Ssum.thy src/HOLCF/Up.thy

2010-10-05 Brian Huffman <brianh@cs.pdx.edu> [Tue, 05 Oct 2010 17:36:45 -0700] rev 39972
add lemmas finite_deflation_imp_compact, cast_below_cast_iff
src/HOLCF/Algebraic.thy src/HOLCF/Bifinite.thy