2014-03-09 haftmann [Sun, 09 Mar 2014 22:45:07 +0100] rev 56014
tuned;
elimination rule subset_imageE;
typical composition collapsing rewrite order in lemma image_image_eq_image_comp;
destruction rules ball_imageD, bex_imageD
src/HOL/Set.thy

2014-03-09 traytel [Sun, 09 Mar 2014 22:27:04 +0100] rev 56013
more careful unfolding of internal constants
src/HOL/Tools/BNF/bnf_comp.ML

2014-03-09 traytel [Sun, 09 Mar 2014 21:40:41 +0100] rev 56012
made typedef for the type of the bound optional (size-based)
src/HOL/Tools/BNF/bnf_comp.ML

2014-03-07 traytel [Fri, 07 Mar 2014 23:10:27 +0100] rev 56011
made natLe{q,ss} constants (yields smaller terms in composition)
src/HOL/BNF_Cardinal_Order_Relation.thy src/HOL/Cardinals/Cardinal_Order_Relation.thy

2014-03-07 traytel [Fri, 07 Mar 2014 23:09:10 +0100] rev 56010
removed junk
src/HOL/Tools/BNF/bnf_comp.ML

2014-03-09 wenzelm [Sun, 09 Mar 2014 18:43:38 +0100] rev 56009
tuned proofs;
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy

2014-03-09 wenzelm [Sun, 09 Mar 2014 17:43:40 +0100] rev 56008
unused;
src/Pure/consts.ML src/Pure/type.ML

2014-03-09 wenzelm [Sun, 09 Mar 2014 17:40:02 +0100] rev 56007
tuned;
src/Pure/Isar/proof_context.ML

2014-03-09 wenzelm [Sun, 09 Mar 2014 17:37:34 +0100] rev 56006
more formal read_root;
src/Pure/Isar/isar_cmd.ML src/Pure/Isar/isar_syn.ML

2014-03-09 wenzelm [Sun, 09 Mar 2014 17:08:31 +0100] rev 56005
simplified / modernized hide commands: proper outer parsers and PIDE markup via check;
src/Pure/Isar/isar_cmd.ML src/Pure/Isar/isar_syn.ML