2014-03-16 haftmann [Sun, 16 Mar 2014 18:09:04 +0100] rev 56166
normalising simp rules for compound operators
NEWS src/HOL/BNF_Comp.thy src/HOL/Complete_Lattices.thy src/HOL/Conditionally_Complete_Lattices.thy src/HOL/Finite_Set.thy src/HOL/GCD.thy src/HOL/Groups_Big.thy src/HOL/Library/Extended_Real.thy src/HOL/Library/FSet.thy src/HOL/Library/Option_ord.thy src/HOL/Library/Product_Order.thy src/HOL/Lifting_Set.thy src/HOL/List.thy src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy src/HOL/Multivariate_Analysis/Integration.thy src/HOL/Multivariate_Analysis/Linear_Algebra.thy src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy src/HOL/Predicate.thy src/HOL/Probability/Caratheodory.thy src/HOL/Probability/Lebesgue_Integration.thy src/HOL/Probability/Probability_Measure.thy src/HOL/Probability/Radon_Nikodym.thy src/HOL/Probability/Regularity.thy src/HOL/Topological_Spaces.thy src/HOL/UNITY/ProgressSets.thy src/HOL/Wellfounded.thy

2014-03-15 wenzelm [Sat, 15 Mar 2014 16:54:32 +0100] rev 56165
tuned markup;
src/Pure/Tools/rail.ML

2014-03-15 wenzelm [Sat, 15 Mar 2014 15:50:41 +0100] rev 56164
minor tuning;
src/Pure/General/name_space.ML

2014-03-15 wenzelm [Sat, 15 Mar 2014 15:49:23 +0100] rev 56163
more markup;
src/Pure/Tools/rail.ML

2014-03-15 wenzelm [Sat, 15 Mar 2014 12:51:14 +0100] rev 56162
clarified completion ordering: prefer local names;
src/Pure/General/completion.scala src/Pure/General/long_name.ML src/Pure/General/name_space.ML

2014-03-15 wenzelm [Sat, 15 Mar 2014 11:59:18 +0100] rev 56161
tuned signature;
eliminated clones;
src/HOL/Mirabelle/Tools/mirabelle.ML src/HOL/Mutabelle/mutabelle.ML src/HOL/Mutabelle/mutabelle_extra.ML src/HOL/Tools/Nitpick/nitpick_hol.ML src/HOL/Tools/Quickcheck/find_unused_assms.ML src/Pure/Proof/proof_checker.ML src/Pure/Proof/proof_syntax.ML src/Pure/global_theory.ML

2014-03-15 wenzelm [Sat, 15 Mar 2014 11:57:55 +0100] rev 56160
tuned -- avoid vacuous reports;
src/Pure/General/name_space.ML

2014-03-15 wenzelm [Sat, 15 Mar 2014 11:28:07 +0100] rev 56159
clarified local facts;
src/Pure/Tools/find_theorems.ML

2014-03-15 wenzelm [Sat, 15 Mar 2014 11:22:25 +0100] rev 56158
more explicit treatment of verbose mode, which includes concealed entries;
src/Doc/IsarRef/Misc.thy src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML src/Pure/Isar/isar_cmd.ML src/Pure/Isar/isar_syn.ML src/Pure/Isar/proof_context.ML src/Pure/Isar/proof_display.ML src/Pure/Tools/find_theorems.ML src/Pure/Tools/proof_general.ML src/Pure/facts.ML

2014-03-15 wenzelm [Sat, 15 Mar 2014 10:29:42 +0100] rev 56157
removed dead code;
src/HOL/Mutabelle/Mutabelle.thy