Thu, 06 Mar 2014 10:12:47 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 05 Mar 2014 19:52:28 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 05 Mar 2014 18:26:35 +0100 |
wenzelm |
more markup for inner syntax class/type names (notably for completion);
|
file |
diff |
annotate
|
Sun, 02 Mar 2014 21:30:47 +0100 |
wenzelm |
prefer Name_Space.check with its builtin reports (including completion);
|
file |
diff |
annotate
|
Sun, 02 Mar 2014 21:13:29 +0100 |
wenzelm |
tuned source structure;
|
file |
diff |
annotate
|
Sun, 02 Mar 2014 21:02:27 +0100 |
wenzelm |
prefer Name_Space.check with its builtin reports (including completion);
|
file |
diff |
annotate
|
Sun, 02 Mar 2014 20:34:11 +0100 |
wenzelm |
consider completion report as part of error message -- less stateful, may get handled;
|
file |
diff |
annotate
|
Sun, 02 Mar 2014 20:20:20 +0100 |
wenzelm |
more markup for read_class: imitate Name_Space.check despite lack of Name_Space.table;
|
file |
diff |
annotate
|
Sat, 01 Mar 2014 23:17:37 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sat, 01 Mar 2014 22:46:31 +0100 |
wenzelm |
clarified language markup: added "delimited" property;
|
file |
diff |
annotate
|
Tue, 25 Feb 2014 11:36:04 +0100 |
wenzelm |
more positions;
|
file |
diff |
annotate
|
Mon, 24 Feb 2014 14:58:40 +0100 |
wenzelm |
prefer standard Proof_Context.transfer, with theory stamp transfer (should now work thanks to purely functional theory, without Theory.copy etc.);
|
file |
diff |
annotate
|
Mon, 03 Feb 2014 16:33:54 +0100 |
wenzelm |
more formal markup;
|
file |
diff |
annotate
|
Tue, 31 Dec 2013 14:29:16 +0100 |
wenzelm |
proper context for norm_hhf and derived operations;
|
file |
diff |
annotate
|
Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
Fri, 13 Dec 2013 20:20:15 +0100 |
wenzelm |
maintain morphism names for diagnostic purposes;
|
file |
diff |
annotate
|
Mon, 16 Sep 2013 23:08:02 +0200 |
wenzelm |
treat all dummy type variables separately (in contrast to fca432074fb2);
|
file |
diff |
annotate
|
Tue, 03 Sep 2013 19:58:00 +0200 |
wenzelm |
cases: formal binding of 'assumes', with position provided via invoke_case;
|
file |
diff |
annotate
|
Tue, 03 Sep 2013 13:09:15 +0200 |
wenzelm |
cases: more position information and PIDE markup;
|
file |
diff |
annotate
|
Wed, 29 May 2013 18:25:11 +0200 |
wenzelm |
tuned signature -- more explicit flags for low-level Thm.bicompose;
|
file |
diff |
annotate
|
Sun, 26 May 2013 19:27:32 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 10 Apr 2013 17:02:47 +0200 |
wenzelm |
added ML antiquotation @{theory_context};
|
file |
diff |
annotate
|
Wed, 03 Apr 2013 13:58:00 +0200 |
wenzelm |
tuned output -- less bullets;
|
file |
diff |
annotate
|
Sat, 30 Mar 2013 13:40:19 +0100 |
wenzelm |
more item markup;
|
file |
diff |
annotate
|
Sat, 30 Mar 2013 12:13:39 +0100 |
wenzelm |
item markup for Proof_Context.pretty_fact;
|
file |
diff |
annotate
|
Mon, 26 Nov 2012 21:46:04 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sun, 25 Nov 2012 19:49:24 +0100 |
wenzelm |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
file |
diff |
annotate
|
Mon, 19 Nov 2012 20:23:47 +0100 |
wenzelm |
theorem status about oracles/futures is no longer printed by default;
|
file |
diff |
annotate
|
Wed, 17 Oct 2012 10:46:14 +0200 |
wenzelm |
more formal markup;
|
file |
diff |
annotate
|
Tue, 09 Oct 2012 19:24:19 +0200 |
wenzelm |
more explicit flags for facts table;
|
file |
diff |
annotate
|
Wed, 03 Oct 2012 17:12:08 +0200 |
wenzelm |
more error positions;
|
file |
diff |
annotate
|
Wed, 03 Oct 2012 14:58:56 +0200 |
wenzelm |
allow position constraints to coexist with 0 or 1 sort constraints;
|
file |
diff |
annotate
|
Mon, 01 Oct 2012 16:37:22 +0200 |
wenzelm |
report sort assignment of visible type variables;
|
file |
diff |
annotate
|
Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
Mon, 02 Apr 2012 19:47:21 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sun, 01 Apr 2012 18:01:19 +0200 |
wenzelm |
tuned signature;
|
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, 17 Mar 2012 23:55:03 +0100 |
wenzelm |
proper naming of simprocs according to actual target context;
|
file |
diff |
annotate
|
Wed, 14 Mar 2012 17:52:38 +0100 |
wenzelm |
source positions for locale and class expressions;
|
file |
diff |
annotate
|
Fri, 09 Mar 2012 20:04:19 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sat, 03 Mar 2012 21:43:59 +0100 |
wenzelm |
canonical argument order for attribute application;
|
file |
diff |
annotate
|
Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
Sun, 27 Nov 2011 21:53:38 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 11 Nov 2011 12:52:57 +0100 |
wenzelm |
more scalable Proof_Context.prepare_sorts;
|
file |
diff |
annotate
|
Wed, 09 Nov 2011 20:47:11 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 09 Nov 2011 17:57:42 +0100 |
wenzelm |
sort assignment before simultaneous term_check, not isolated parse_term;
|
file |
diff |
annotate
|
Thu, 03 Nov 2011 23:55:53 +0100 |
wenzelm |
more general Proof_Context.bind_propp, which allows outer parameters;
|
file |
diff |
annotate
|
Thu, 03 Nov 2011 22:23:41 +0100 |
wenzelm |
tuned signature -- canonical argument order;
|
file |
diff |
annotate
|
Wed, 13 Jul 2011 20:36:18 +0200 |
wenzelm |
sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML);
|
file |
diff |
annotate
|
Sat, 25 Jun 2011 19:38:35 +0200 |
wenzelm |
entity markup for "type", "constant";
|
file |
diff |
annotate
|
Sat, 25 Jun 2011 18:15:36 +0200 |
wenzelm |
type classes: entity markup instead of old-style token markup;
|
file |
diff |
annotate
|
Thu, 12 May 2011 16:23:13 +0200 |
wenzelm |
proper configuration options Proof_Context.debug and Proof_Context.verbose;
|
file |
diff |
annotate
|
Thu, 28 Apr 2011 21:06:04 +0200 |
wenzelm |
literal facts `prop` may contain dummy patterns;
|
file |
diff |
annotate
|
Thu, 28 Apr 2011 20:20:49 +0200 |
wenzelm |
eliminated slightly odd Proof_Context.bind_fixes;
|
file |
diff |
annotate
|
Wed, 27 Apr 2011 23:02:43 +0200 |
wenzelm |
more precise positions via binding;
|
file |
diff |
annotate
|
Wed, 27 Apr 2011 20:58:40 +0200 |
wenzelm |
tuned signature -- eliminated odd comment;
|
file |
diff |
annotate
|
Wed, 27 Apr 2011 20:19:05 +0200 |
wenzelm |
more precise position information via Variable.add_fixes_binding;
|
file |
diff |
annotate
|
Wed, 27 Apr 2011 17:58:45 +0200 |
wenzelm |
reorganized fixes as specialized (global) name space;
|
file |
diff |
annotate
|
Sat, 23 Apr 2011 18:46:01 +0200 |
wenzelm |
clarified Consts.read_const;
|
file |
diff |
annotate
|
Sat, 23 Apr 2011 18:25:50 +0200 |
wenzelm |
clarified Type.the_decl;
|
file |
diff |
annotate
|