2010-03-06 haftmann [Sat, 06 Mar 2010 15:31:31 +0100] rev 35619
lemma restrict_complement_singleton_eq
src/HOL/Map.thy

2010-03-06 haftmann [Sat, 06 Mar 2010 15:31:30 +0100] rev 35618
some lemma refinements
src/HOL/Library/RBT.thy

2010-03-06 haftmann [Sat, 06 Mar 2010 15:31:30 +0100] rev 35617
added Table.thy
src/HOL/IsaMakefile src/HOL/Library/Library.thy src/HOL/Library/Table.thy src/HOL/ex/Codegenerator_Candidates.thy

2010-03-06 wenzelm [Sat, 06 Mar 2010 17:53:04 +0100] rev 35616
provide ProofContext.def_type depending on "pattern" mode;
src/Pure/Isar/proof_context.ML

2010-03-06 wenzelm [Sat, 06 Mar 2010 17:32:45 +0100] rev 35615
record_type_tr': more robust strip_fields (printed types are not necessarily well-formed, e.g. in Syntax.pretty_arity);
src/HOL/Tools/record.ML

2010-03-06 wenzelm [Sat, 06 Mar 2010 16:13:22 +0100] rev 35614
record_type_abbr_tr': removed obsolete workaround for decode_type, which now retains syntactic categories of variables vs. constructors (authentic syntax);
src/HOL/Tools/record.ML

2010-03-06 wenzelm [Sat, 06 Mar 2010 15:39:16 +0100] rev 35613
eliminated Args.bang_facts (legacy feature);
NEWS doc-src/IsarRef/Thy/Generic.thy doc-src/IsarRef/Thy/HOL_Specific.thy doc-src/IsarRef/Thy/document/Generic.tex doc-src/IsarRef/Thy/document/HOL_Specific.tex src/Provers/blast.ML src/Provers/clasimp.ML src/Provers/classical.ML src/Pure/Isar/args.ML src/Pure/simplifier.ML

2010-03-06 wenzelm [Sat, 06 Mar 2010 15:34:29 +0100] rev 35612
eliminated old-style prems;
tuned proofs;
src/HOL/Matrix/Matrix.thy

2010-03-06 wenzelm [Sat, 06 Mar 2010 14:35:06 +0100] rev 35611
removed unused term_lift_inst_rule (superceded by Subgoal.FOCUS etc.);
src/Pure/tactic.ML

2010-03-06 wenzelm [Sat, 06 Mar 2010 14:28:31 +0100] rev 35610
Some notes on platform support of Isabelle.
Admin/PLATFORMS