wenzelm [Sun, 08 Mar 2009 21:12:37 +0100] rev 30368
added (raw_)antiquotation -- simplified wrapper for defining output commands;
wenzelm [Sun, 08 Mar 2009 20:31:54 +0100] rev 30367
simplified presentation: pass state directly;
wenzelm [Sun, 08 Mar 2009 20:31:01 +0100] rev 30366
simplified presentation: built into transaction, pass state directly;
wenzelm [Sun, 08 Mar 2009 17:37:18 +0100] rev 30365
adapted to structure Long_Name;
wenzelm [Sun, 08 Mar 2009 17:26:14 +0100] rev 30364
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm [Sun, 08 Mar 2009 17:19:15 +0100] rev 30363
proper local context for text with antiquotations;
wenzelm [Sun, 08 Mar 2009 17:05:43 +0100] rev 30362
more explicit warning message;
wenzelm [Sun, 08 Mar 2009 17:03:07 +0100] rev 30361
added qualified_name -- emulates old-style qualified bstring;
tuned;
wenzelm [Sun, 08 Mar 2009 16:53:38 +0100] rev 30360
added General/long_name.ML;
wenzelm [Sun, 08 Mar 2009 16:53:07 +0100] rev 30359
moved basic algebra of long names from structure NameSpace to Long_Name;
tuned signature;
wenzelm [Sun, 08 Mar 2009 15:01:10 +0100] rev 30358
index_ML: removed spurious writeln introduced in 41ce4f5c97c9 -- it merely produces unreadable LaTeX sources;
wenzelm [Sun, 08 Mar 2009 12:16:12 +0100] rev 30357
proper context for Simplifier.pretty_ss;
wenzelm [Sun, 08 Mar 2009 12:15:58 +0100] rev 30356
added dest_ss;
proper context fo pretty_ss;
tuned;
wenzelm [Sun, 08 Mar 2009 00:41:52 +0100] rev 30355
use binding type;
wenzelm [Sun, 08 Mar 2009 00:16:34 +0100] rev 30354
merged
haftmann [Sat, 07 Mar 2009 23:41:04 +0100] rev 30353
merged
haftmann [Sat, 07 Mar 2009 15:20:32 +0100] rev 30352
restructured theory Set.thy
wenzelm [Sat, 07 Mar 2009 23:37:09 +0100] rev 30351
merged
blanchet [Sat, 07 Mar 2009 17:05:40 +0100] rev 30350
Removed "nitpick_maybe" constant. Makarius now taught me a much nicer trick.
blanchet [Sat, 07 Mar 2009 16:47:36 +0100] rev 30349
Added a second timeout mechanism to Refute.
For some reason, TimeLimit.timeLimit often does not work, and it
leaves Refute running forever, making any evaluation using
Mutabelle or Mirabelle impossible. The redundant timeout seems to
do the trick.
blanchet [Sat, 07 Mar 2009 12:27:26 +0100] rev 30348
merged
blanchet [Sat, 07 Mar 2009 12:26:56 +0100] rev 30347
Refute: Distinguish between "genuine" and "potential" in the newly added "expect" option.
wenzelm [Sat, 07 Mar 2009 23:30:58 +0100] rev 30346
minimal adaptions for abstract binding type;
wenzelm [Sat, 07 Mar 2009 22:17:25 +0100] rev 30345
more uniform handling of binding in packages;
wenzelm [Sat, 07 Mar 2009 22:16:50 +0100] rev 30344
more uniform handling of binding in targets and derived elements;
wenzelm [Sat, 07 Mar 2009 22:12:07 +0100] rev 30343
replace old bstring by binding for logical primitives: class, type, const etc.;
wenzelm [Sat, 07 Mar 2009 22:04:59 +0100] rev 30342
moved Thm.def_name(_optional) to more_thm.ML;
moved old-style Thm.get_def to Drule.get_def;
wenzelm [Sat, 07 Mar 2009 21:57:36 +0100] rev 30341
adapted Syntax.const_name;
wenzelm [Sat, 07 Mar 2009 21:20:17 +0100] rev 30340
canonical argument order for type_name, const_name;
wenzelm [Sat, 07 Mar 2009 21:19:24 +0100] rev 30339
added const_binding;