Fri, 17 May 2013 20:41:45 +0200 |
wenzelm |
proper option quick_and_dirty;
|
file |
diff |
annotate
|
Sat, 30 Mar 2013 13:40:19 +0100 |
wenzelm |
more item markup;
|
file |
diff |
annotate
|
Wed, 27 Mar 2013 14:50:30 +0100 |
wenzelm |
clarified Skip_Proof.cheat_tac: more standard tactic;
|
file |
diff |
annotate
|
Sat, 09 Mar 2013 13:01:24 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 30 Nov 2012 22:38:06 +0100 |
wenzelm |
print formal entities with markup;
|
file |
diff |
annotate
|
Wed, 17 Oct 2012 13:20:08 +0200 |
wenzelm |
more method position information, notably finished_pos after end of previous text;
|
file |
diff |
annotate
|
Tue, 16 Oct 2012 20:23:00 +0200 |
wenzelm |
more proof method text position information;
|
file |
diff |
annotate
|
Tue, 16 Oct 2012 17:47:23 +0200 |
wenzelm |
clarified defer/prefer: more specific errors;
|
file |
diff |
annotate
|
Sat, 13 Oct 2012 18:04:11 +0200 |
wenzelm |
refined Proof.the_finished_goal with more informative error;
|
file |
diff |
annotate
|
Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
Sun, 18 Mar 2012 13:04:22 +0100 |
wenzelm |
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
|
file |
diff |
annotate
|
Sat, 03 Mar 2012 21:43:59 +0100 |
wenzelm |
canonical argument order for attribute application;
|
file |
diff |
annotate
|
Tue, 14 Feb 2012 19:51:39 +0100 |
wenzelm |
tuned signature, according to actual usage of these operations;
|
file |
diff |
annotate
|
Sun, 06 Nov 2011 21:51:46 +0100 |
wenzelm |
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
|
file |
diff |
annotate
|
Fri, 21 Oct 2011 11:26:14 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sun, 15 May 2011 17:06:35 +0200 |
wenzelm |
optional description for 'attribute_setup' and 'method_setup';
|
file |
diff |
annotate
|
Mon, 02 May 2011 16:33:21 +0200 |
wenzelm |
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
|
file |
diff |
annotate
|
Sun, 17 Apr 2011 21:17:45 +0200 |
wenzelm |
markup attributes/methods via name space;
|
file |
diff |
annotate
|
Sun, 17 Apr 2011 19:54:04 +0200 |
wenzelm |
report Name_Space.declare/define, relatively to context;
|
file |
diff |
annotate
|
Sat, 16 Apr 2011 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
Sat, 16 Apr 2011 13:48:45 +0200 |
wenzelm |
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
|
file |
diff |
annotate
|
Tue, 21 Dec 2010 21:54:51 +0100 |
wenzelm |
configuration option "rule_trace";
|
file |
diff |
annotate
|
Fri, 17 Sep 2010 20:18:27 +0200 |
wenzelm |
tuned signature of (Context_)Position.report variants;
|
file |
diff |
annotate
|
Mon, 31 May 2010 21:06:57 +0200 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
Sun, 30 May 2010 21:34:19 +0200 |
wenzelm |
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
|
file |
diff |
annotate
|
Mon, 17 May 2010 15:11:25 +0200 |
wenzelm |
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
|
file |
diff |
annotate
|
Sat, 15 May 2010 23:16:32 +0200 |
wenzelm |
refer directly to structure Keyword and Parse;
|
file |
diff |
annotate
|
Wed, 07 Apr 2010 19:17:10 +0200 |
ballarin |
Merged resolving conflicts NEWS and locale.ML.
|
file |
diff |
annotate
|
Mon, 15 Feb 2010 01:34:08 +0100 |
ballarin |
Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
|
file |
diff |
annotate
|
Sun, 07 Mar 2010 12:19:47 +0100 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|