2014-07-24 wenzelm [Thu, 24 Jul 2014 11:54:15 +0200] rev 57641
more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy);
src/HOL/BNF_Def.thy src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy src/HOL/BNF_Examples/Stream_Processor.thy src/HOL/BNF_FP_Base.thy src/HOL/BNF_LFP.thy src/HOL/Main.thy

2014-07-24 wenzelm [Thu, 24 Jul 2014 11:51:22 +0200] rev 57640
reconfirm continuous checking on startup, to address common trap of disabling it accidentally;
src/Tools/jEdit/src/plugin.scala

2014-07-24 wenzelm [Thu, 24 Jul 2014 11:46:40 +0200] rev 57639
tuned;
src/Pure/GUI/gui.scala

2014-07-24 wenzelm [Thu, 24 Jul 2014 10:38:46 +0200] rev 57638
less authentic SHA1.digest: trust Scala side on blobs and avoid re-calculation via Foreign Language Interface, which might be a cause of problems;
src/Pure/General/sha1.ML src/Pure/General/sha1.scala src/Pure/General/sha1_polyml.ML src/Pure/PIDE/document.ML

2014-07-24 wenzelm [Thu, 24 Jul 2014 10:22:34 +0200] rev 57637
updated NEWS according to d38a98f496dd (see also bdc2c6b40bf2);
NEWS

2014-07-24 blanchet [Thu, 24 Jul 2014 00:24:00 +0200] rev 57636
stick to external proofs when invoking E, because they are more detailed and do not merge steps
src/Doc/Sledgehammer/document/root.tex src/HOL/Tools/ATP/atp_systems.ML

2014-07-24 blanchet [Thu, 24 Jul 2014 00:24:00 +0200] rev 57635
more robust handling of types for skolems (modeled as Frees)
src/HOL/Tools/ATP/atp_proof_reconstruct.ML src/HOL/Tools/ATP/atp_waldmeister.ML

2014-07-24 blanchet [Thu, 24 Jul 2014 00:24:00 +0200] rev 57634
tuning
src/HOL/BNF_Examples/Compat.thy src/HOL/BNF_Examples/IsaFoR_Datatypes.thy src/HOL/BNF_Examples/Koenig.thy src/HOL/BNF_Examples/Stream_Processor.thy

2014-07-24 blanchet [Thu, 24 Jul 2014 00:24:00 +0200] rev 57633
repaired named derivations
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML src/HOL/Tools/BNF/bnf_lfp_compat.ML src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML

2014-07-24 blanchet [Thu, 24 Jul 2014 00:24:00 +0200] rev 57632
use the noted theorems in 'BNF_Comp'
src/HOL/Tools/BNF/bnf_comp.ML src/HOL/Tools/BNF/bnf_def.ML