2015-07-25 wenzelm [Sat, 25 Jul 2015 23:15:37 +0200] rev 60780
more accurate maxidx;
src/Pure/drule.ML

2015-07-25 wenzelm [Sat, 25 Jul 2015 21:54:09 +0200] rev 60779
clarified error;
src/Pure/drule.ML

2015-07-25 wenzelm [Sat, 25 Jul 2015 21:37:09 +0200] rev 60778
added infer_instantiate, which is meant to supersede cterm_instantiate;
src/Pure/drule.ML

2015-07-24 wenzelm [Fri, 24 Jul 2015 22:29:06 +0200] rev 60777
eliminated alias;
src/HOL/Tools/BNF/bnf_gfp_tactics.ML src/HOL/Tools/BNF/bnf_lfp_tactics.ML src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML

2015-07-24 wenzelm [Fri, 24 Jul 2015 22:20:22 +0200] rev 60776
proper context;
src/Pure/tactic.ML

2015-07-24 wenzelm [Fri, 24 Jul 2015 22:19:36 +0200] rev 60775
unused;
src/Pure/tactic.ML

2015-07-24 wenzelm [Fri, 24 Jul 2015 22:16:39 +0200] rev 60774
proper context;
src/FOLP/simp.ML src/FOLP/simpdata.ML src/HOL/Library/old_recdef.ML src/HOL/Tools/Old_Datatype/old_datatype.ML src/HOL/Tools/Old_Datatype/old_rep_datatype.ML src/HOL/UNITY/UNITY_tactics.ML src/HOL/ex/MT.thy src/Provers/quantifier1.ML src/Pure/tactic.ML src/ZF/Tools/inductive_package.ML src/ZF/Tools/typechk.ML src/ZF/UNITY/SubstAx.thy

2015-07-23 wenzelm [Thu, 23 Jul 2015 22:13:42 +0200] rev 60773
more symbols by default, without xsymbols mode;
src/HOL/Algebra/FiniteProduct.thy src/HOL/Algebra/Ring.thy src/HOL/MicroJava/BV/Correct.thy src/HOL/MicroJava/Comp/TranslCompTp.thy src/HOL/Number_Theory/MiscAlgebra.thy src/HOL/UNITY/Comp/Alloc.thy src/HOL/UNITY/Comp/AllocImpl.thy src/HOL/UNITY/Comp/Client.thy src/HOL/UNITY/Comp/Handshake.thy src/HOL/UNITY/Comp/Priority.thy src/HOL/UNITY/Lift_prog.thy src/HOL/UNITY/PPROD.thy src/HOL/UNITY/Rename.thy src/HOL/UNITY/SubstAx.thy src/HOL/UNITY/Union.thy src/HOL/UNITY/WFair.thy

2015-07-23 hoelzl [Thu, 23 Jul 2015 16:40:47 +0200] rev 60772
Measures form a CCPO
src/HOL/Library/Extended_Real.thy src/HOL/Probability/Measure_Space.thy src/HOL/Probability/Sigma_Algebra.thy

2015-07-23 hoelzl [Thu, 23 Jul 2015 16:39:10 +0200] rev 60771
reorganized Extended_Real
src/HOL/Library/Extended_Real.thy src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy src/HOL/Probability/Borel_Space.thy