2011-02-18 wenzelm [Fri, 18 Feb 2011 16:22:27 +0100] rev 41777
more precise headers;
src/FOL/ex/If.thy src/FOL/ex/Quantifiers_Cla.thy src/FOLP/ex/Foundation.thy src/FOLP/ex/Nat.thy src/HOL/ZF/Games.thy src/ZF/AC/AC17_AC1.thy src/ZF/ArithSimp.thy src/ZF/Bool.thy src/ZF/Datatype_ZF.thy src/ZF/Int_ZF.thy src/ZF/OrdQuant.thy src/ZF/Sum.thy src/ZF/ex/Commutation.thy src/ZF/ex/NatSum.thy src/ZF/pair.thy

2011-02-18 wenzelm [Fri, 18 Feb 2011 16:11:58 +0100] rev 41776
less verbose tracing;
src/Pure/Concurrent/future.ML src/Pure/goal.ML

2011-02-18 wenzelm [Fri, 18 Feb 2011 16:07:32 +0100] rev 41775
standardized headers;
src/HOL/Auth/Guard/Analz.thy src/HOL/Auth/Guard/Extensions.thy src/HOL/Auth/Guard/Guard.thy src/HOL/Auth/Guard/GuardK.thy src/HOL/Auth/Guard/Guard_NS_Public.thy src/HOL/Auth/Guard/Guard_OtwayRees.thy src/HOL/Auth/Guard/Guard_Public.thy src/HOL/Auth/Guard/Guard_Shared.thy src/HOL/Auth/Guard/Guard_Yahalom.thy src/HOL/Auth/Guard/List_Msg.thy src/HOL/Auth/Guard/P1.thy src/HOL/Auth/Guard/P2.thy src/HOL/Auth/Guard/Proto.thy

2011-02-18 wenzelm [Fri, 18 Feb 2011 15:46:13 +0100] rev 41774
modernized specifications;
src/HOL/Auth/Guard/Proto.thy src/HOL/Auth/KerberosIV.thy src/HOL/Auth/KerberosIV_Gets.thy src/HOL/Auth/KerberosV.thy src/HOL/Auth/Message.thy src/HOL/Auth/Public.thy src/HOL/Auth/Smartcard/ShoupRubin.thy src/HOL/Auth/Smartcard/ShoupRubinBella.thy src/HOL/Auth/Smartcard/Smartcard.thy src/HOL/Auth/TLS.thy

2011-02-18 blanchet [Fri, 18 Feb 2011 16:30:44 +0100] rev 41773
gracious timeout in "blocking" mode
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML

2011-02-18 blanchet [Fri, 18 Feb 2011 16:19:08 +0100] rev 41772
make Nitpick's timeout mechanism somewhat more reliable/friendly;
avoid producing warnings when invoked in "auto" mode
src/HOL/Tools/Nitpick/nitpick.ML

2011-02-18 blanchet [Fri, 18 Feb 2011 15:44:52 +0100] rev 41771
better fudge factors for Sledgehammer
src/HOL/Tools/SMT/smt_setup_solvers.ML

2011-02-18 blanchet [Fri, 18 Feb 2011 15:17:39 +0100] rev 41770
adjust fudge factors
src/HOL/Tools/ATP/atp_systems.ML src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML

2011-02-18 blanchet [Fri, 18 Feb 2011 12:32:55 +0100] rev 41769
extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs
src/HOL/Tools/ATP/atp_problem.ML src/HOL/Tools/ATP/atp_systems.ML src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML

2011-02-17 blanchet [Thu, 17 Feb 2011 12:14:47 +0100] rev 41768
export more functionality of Sledgehammer to applications (for experiments)
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML