wenzelm [Mon, 15 Aug 2011 20:19:41 +0200] rev 44199
retrieve imports from document state, with fall-back on theory loader for preloaded theories;
misc tuning;
wenzelm [Mon, 15 Aug 2011 19:27:55 +0200] rev 44198
explicit check of finished evaluation;
wenzelm [Mon, 15 Aug 2011 16:38:42 +0200] rev 44197
refined Document.edit: less stateful update via Graph.schedule;
clarified node result -- more direct get_theory;
clarified Document.joint_commands;
wenzelm [Mon, 15 Aug 2011 14:54:36 +0200] rev 44196
simplified exec: eliminated unused status flag;
huffman [Sun, 14 Aug 2011 08:45:38 -0700] rev 44195
consistently use variable name 'F' for filters
huffman [Sun, 14 Aug 2011 07:54:24 -0700] rev 44194
generalize lemmas about LIM and LIMSEQ to tendsto
huffman [Sat, 13 Aug 2011 18:10:14 -0700] rev 44193
HOL-Nominal-Examples: respect distinction between sets and functions
wenzelm [Sat, 13 Aug 2011 22:04:07 +0200] rev 44192
less verbosity in batch mode -- spam reduction and notable performance improvement;
clarified Proof_Display.print_consts;
wenzelm [Sat, 13 Aug 2011 21:28:01 +0200] rev 44191
merged
huffman [Sat, 13 Aug 2011 07:56:55 -0700] rev 44190
HOL-Hahn_Banach: use Set_Algebras library