2015-05-17 wenzelm [Sun, 17 May 2015 23:03:49 +0200] rev 60288
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
NEWS doc/Contents src/Doc/Eisbach/Base.thy src/Doc/Eisbach/Manual.thy src/Doc/Eisbach/Preface.thy src/Doc/Eisbach/document/build src/Doc/Eisbach/document/root.tex src/Doc/Eisbach/document/style.sty src/Doc/ROOT

2015-05-17 wenzelm [Sun, 17 May 2015 22:33:34 +0200] rev 60287
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
src/HOL/Eisbach/Tests.thy src/HOL/Eisbach/match_method.ML src/HOL/Eisbach/method_closure.ML

2015-05-17 wenzelm [Sun, 17 May 2015 21:44:34 +0200] rev 60286
tuned;
src/Doc/Isar_Ref/Document_Preparation.thy src/Doc/Isar_Ref/Preface.thy src/Doc/Isar_Ref/document/root.tex

2015-05-16 wenzelm [Sat, 16 May 2015 12:05:52 +0200] rev 60285
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
src/HOL/Eisbach/Eisbach.thy src/HOL/Eisbach/Eisbach_Tools.thy src/HOL/Eisbach/Examples.thy src/HOL/Eisbach/Tests.thy src/HOL/Eisbach/eisbach_rule_insts.ML src/HOL/Eisbach/match_method.ML src/HOL/Eisbach/method_closure.ML src/HOL/Eisbach/parse_tools.ML

2015-05-13 wenzelm [Wed, 13 May 2015 19:12:59 +0200] rev 60284
clarified alias: proper update of new accesses instead of conservative insert (via merge), otherwise "local.foo" could take precedence over "foo";
src/Pure/General/name_space.ML

2015-05-13 wenzelm [Wed, 13 May 2015 17:36:33 +0200] rev 60283
tuned whitespace;
src/Pure/Isar/generic_target.ML

2015-05-13 wenzelm [Wed, 13 May 2015 17:27:12 +0200] rev 60282
more permissive operation: allow to print undeclared name space entries, e.g. print_simpset with "record" simproc;
src/Pure/General/name_space.ML

2015-05-09 wenzelm [Sat, 09 May 2015 20:40:28 +0200] rev 60281
Added tag Isabelle2015-RC4 for changeset 05fe9bdc4f8f
.hgtags

2015-05-09 blanchet [Sat, 09 May 2015 10:06:14 +0200] rev 60280
new CVC4 component
Admin/components/components.sha1 Admin/components/main

2015-05-09 blanchet [Sat, 09 May 2015 14:10:10 +0200] rev 60279
took out unreliable 'blast' from tactic altogether
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML