wenzelm [Thu, 19 Mar 2009 13:28:55 +0100] rev 30585
use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
wenzelm [Thu, 19 Mar 2009 13:26:19 +0100] rev 30584
Name.of_binding: proper full_name (with checks) before projecting base name;
wenzelm [Thu, 19 Mar 2009 11:51:49 +0100] rev 30583
merged
huffman [Thu, 19 Mar 2009 01:29:19 -0700] rev 30582
imported patch euclidean
ballarin [Wed, 18 Mar 2009 22:17:23 +0100] rev 30581
Merged.
ballarin [Wed, 18 Mar 2009 22:14:58 +0100] rev 30580
Updated chapters 1-5 to locale reimplementation.
wenzelm [Thu, 19 Mar 2009 11:47:05 +0100] rev 30579
command 'use', 'ML': apply ML environment to theory and target as well;
tuned command descriptions;
wenzelm [Thu, 19 Mar 2009 11:44:34 +0100] rev 30578
added map_contexts (cf. Proof.map_contexts);
wenzelm [Thu, 19 Mar 2009 11:20:22 +0100] rev 30577
tuned;
wenzelm [Wed, 18 Mar 2009 22:41:15 +0100] rev 30576
generalized ML_Context.inherit_env;
wenzelm [Wed, 18 Mar 2009 22:41:14 +0100] rev 30575
more precise type Symbol_Pos.text;
wenzelm [Wed, 18 Mar 2009 22:41:14 +0100] rev 30574
more precise type Symbol_Pos.text;
geralized ML_Context.inherit_env;
wenzelm [Wed, 18 Mar 2009 21:55:38 +0100] rev 30573
de-camelized Symbol_Pos;
wenzelm [Wed, 18 Mar 2009 20:03:01 +0100] rev 30572
Library.merge/OrdList.union: optimize the important special case where the tables coincide -- NOTE: this changes both the operational behaviour and the result for non-standard eq/ord notion;
wenzelm [Wed, 18 Mar 2009 19:11:26 +0100] rev 30571
reduced verbosity;
haftmann [Wed, 18 Mar 2009 15:23:52 +0100] rev 30570
made SML/NJ happy
haftmann [Wed, 18 Mar 2009 11:57:28 +0100] rev 30569
tuned interpunctation
wenzelm [Tue, 17 Mar 2009 19:53:57 +0100] rev 30568
strip_abss: always strip abstractions as far as possible, without keeping alternatives (which appear to be redundant anyway, but cause significant slowdown since discrimination nets collapse abstractions);
wenzelm [Tue, 17 Mar 2009 19:06:04 +0100] rev 30567
close/all_assm_tac: finish all subgoals from left to right (cf. Proof.goal_tac a28d83e903ce) -- NB: ALLGOALS/THEN_ALL_NEW operate from right to left;
wenzelm [Tue, 17 Mar 2009 16:55:21 +0100] rev 30566
reverted abbreviations: improved performance via Item_Net.T;
wenzelm [Tue, 17 Mar 2009 15:35:27 +0100] rev 30565
export match_rew -- useful for implementing "procs" for rewrite_term;
wenzelm [Tue, 17 Mar 2009 15:34:42 +0100] rev 30564
tuned comment;
wenzelm [Tue, 17 Mar 2009 14:14:25 +0100] rev 30563
merged
huffman [Mon, 16 Mar 2009 15:58:41 -0700] rev 30562
document new additions to HOL/Library
huffman [Mon, 16 Mar 2009 15:10:59 -0700] rev 30561
clean up proofs
wenzelm [Tue, 17 Mar 2009 14:12:43 +0100] rev 30560
adapted to general Item_Net;
wenzelm [Tue, 17 Mar 2009 14:12:06 +0100] rev 30559
turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm [Tue, 17 Mar 2009 14:09:20 +0100] rev 30558
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
wenzelm [Tue, 17 Mar 2009 13:33:21 +0100] rev 30557
goal_tac: finish marked assumptions from left to right -- corresponds better with the strategy of etac, with significant performance gains in some situations;
wenzelm [Tue, 17 Mar 2009 12:10:42 +0100] rev 30556
eq_assumption: slightly more efficient by checking (open) result of Logic.assum_problems directly;
tuned;