wenzelm [Thu, 12 Aug 2010 13:49:08 +0200] rev 38360
specific Session.Commands_Changed;
wenzelm [Thu, 12 Aug 2010 13:43:55 +0200] rev 38359
consider snapshot as service of Session, not Document.Change;
wenzelm [Thu, 12 Aug 2010 13:42:05 +0200] rev 38358
tuned scope;
wenzelm [Wed, 11 Aug 2010 23:46:38 +0200] rev 38357
Document.print_id;
wenzelm [Wed, 11 Aug 2010 23:29:17 +0200] rev 38356
consider command state as part of Snapshot, not Document;
wenzelm [Wed, 11 Aug 2010 22:41:26 +0200] rev 38355
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm [Wed, 11 Aug 2010 18:44:06 +0200] rev 38354
Named_Target;
wenzelm [Wed, 11 Aug 2010 18:41:06 +0200] rev 38353
modernized specifications;
tuned headers;
wenzelm [Wed, 11 Aug 2010 18:22:14 +0200] rev 38352
spelling;
wenzelm [Wed, 11 Aug 2010 18:17:53 +0200] rev 38351
merged
haftmann [Wed, 11 Aug 2010 14:45:38 +0200] rev 38350
renamed Theory_Target to the more appropriate Named_Target
haftmann [Wed, 11 Aug 2010 14:41:16 +0200] rev 38349
discontinue old implementation of `foundation`
haftmann [Wed, 11 Aug 2010 14:31:43 +0200] rev 38348
moved instantiation target formally to class_target.ML
haftmann [Wed, 11 Aug 2010 14:31:40 +0200] rev 38347
NEWS
haftmann [Wed, 11 Aug 2010 14:20:34 +0200] rev 38346
merged
haftmann [Wed, 11 Aug 2010 14:19:32 +0200] rev 38345
print fcomp combinator only monadic in connection with other monadic expressions
haftmann [Wed, 11 Aug 2010 14:19:52 +0200] rev 38344
merged
haftmann [Wed, 11 Aug 2010 13:31:29 +0200] rev 38343
merged
haftmann [Wed, 11 Aug 2010 12:30:48 +0200] rev 38342
moved overloading target formally to overloading.ML
haftmann [Wed, 11 Aug 2010 12:24:24 +0200] rev 38341
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann [Wed, 11 Aug 2010 12:04:49 +0200] rev 38340
merged
haftmann [Wed, 11 Aug 2010 08:59:41 +0200] rev 38339
whitespace tuning
haftmann [Wed, 11 Aug 2010 08:58:18 +0200] rev 38338
remove overloading and instantiation from data slot
wenzelm [Wed, 11 Aug 2010 18:11:07 +0200] rev 38337
removed obsolete Toplevel.enter_proof_body;
wenzelm [Wed, 11 Aug 2010 18:10:39 +0200] rev 38336
standardized pretty printing of consts (e.g. see find_theorems, print_theory);
wenzelm [Wed, 11 Aug 2010 18:03:02 +0200] rev 38335
misc tuning and simplification;
wenzelm [Wed, 11 Aug 2010 17:50:29 +0200] rev 38334
simplified/unified command setup;
wenzelm [Wed, 11 Aug 2010 17:37:04 +0200] rev 38333
removed obsolete Proof.get_thmss_cmd (cf. Attrib.eval_thms);
wenzelm [Wed, 11 Aug 2010 17:31:56 +0200] rev 38332
prefer plain Attrib.eval_thmss -- also means the assert_forward of Proof.get_thmss_cmd is skipped, leading to uniform (albeit odd) behaviour concerning forward chaining;
tuned;
wenzelm [Wed, 11 Aug 2010 17:29:54 +0200] rev 38331
prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm [Wed, 11 Aug 2010 17:24:57 +0200] rev 38330
tuned eval_thms (cf. note etc. in proof.ML);
wenzelm [Wed, 11 Aug 2010 15:17:13 +0200] rev 38329
use Pretty.enum convenience;
wenzelm [Wed, 11 Aug 2010 15:00:31 +0200] rev 38328
tuned whitespace;
wenzelm [Wed, 11 Aug 2010 13:39:36 +0200] rev 38327
more precise and more maintainable dependencies;
wenzelm [Wed, 11 Aug 2010 12:50:33 +0200] rev 38326
merged, resolving conflict in src/Pure/IsaMakefile concerning General/xml_data.ML;
haftmann [Wed, 11 Aug 2010 12:04:06 +0200] rev 38325
* -> prod
haftmann [Wed, 11 Aug 2010 12:03:57 +0200] rev 38324
added .ML extension
haftmann [Wed, 11 Aug 2010 11:56:57 +0200] rev 38323
avoid old unnamed infix
haftmann [Wed, 11 Aug 2010 11:52:40 +0200] rev 38322
avoid inclusion of Natural module in generated code
haftmann [Wed, 11 Aug 2010 09:06:31 +0200] rev 38321
explicit ML extension
haftmann [Wed, 11 Aug 2010 08:50:20 +0200] rev 38320
merged
haftmann [Tue, 10 Aug 2010 16:03:54 +0200] rev 38319
separate initialisation for overloading and instantiation target
haftmann [Tue, 10 Aug 2010 15:38:33 +0200] rev 38318
different foundations for different targets; simplified syntax handling of abbreviations
Christian Urban <urbanc@in.tum.de> [Wed, 11 Aug 2010 13:30:24 +0800] rev 38317
deleted duplicate lemma
ballarin [Tue, 10 Aug 2010 22:26:23 +0200] rev 38316
Revert performance improvement of 8ed3a5fb4d25 since it breaks notes element declarations.
haftmann [Tue, 10 Aug 2010 15:09:39 +0200] rev 38315
basic renumbering
haftmann [Tue, 10 Aug 2010 15:07:39 +0200] rev 38314
avoiding redundant primes
haftmann [Tue, 10 Aug 2010 14:57:58 +0200] rev 38313
separated type from term parameters