| Tue, 23 Apr 2013 11:14:50 +0200 |
haftmann |
target-sensitive user-level commands interpretation and sublocale
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 14:43:28 +0100 |
wenzelm |
tuned command descriptions;
|
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
|
| Wed, 10 Oct 2012 15:21:26 +0200 |
wenzelm |
more explicit namespace prefix for 'statespace' -- duplicate facts;
|
file |
diff |
annotate
|
| Thu, 09 Aug 2012 12:39:05 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 18:20:12 +0100 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 20:07:00 +0100 |
wenzelm |
prefer formally checked @{keyword} parser;
|
file |
diff |
annotate
|
| Wed, 14 Mar 2012 20:34:20 +0100 |
wenzelm |
locale expressions without source positions;
|
file |
diff |
annotate
|
| Fri, 02 Dec 2011 15:23:27 +0100 |
wenzelm |
eliminated some legacy operations;
|
file |
diff |
annotate
|
| Mon, 28 Nov 2011 17:06:20 +0100 |
wenzelm |
tuned messages;
|
file |
diff |
annotate
|
| Sun, 06 Nov 2011 17:53:32 +0100 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Sun, 06 Nov 2011 17:05:45 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 22:17:30 +0200 |
wenzelm |
uniform Local_Theory.declaration with explicit params;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 20:53:43 +0200 |
wenzelm |
old term operations are legacy;
|
file |
diff |
annotate
|
| Wed, 29 Jun 2011 20:39:41 +0200 |
wenzelm |
simplified/unified Simplifier.mk_solver;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 16:34:49 +0200 |
wenzelm |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 15:56:57 +0200 |
wenzelm |
more robust exception pattern General.Subscript;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 17:58:45 +0200 |
wenzelm |
reorganized fixes as specialized (global) name space;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 20:49:48 +0200 |
wenzelm |
proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 18:11:20 +0200 |
wenzelm |
eliminated old List.nth;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 14:20:57 +0200 |
wenzelm |
discontinued special treatment of structure Mixfix;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2011 23:04:00 +0200 |
wenzelm |
separate structure Term_Position;
|
file |
diff |
annotate
|
| Tue, 22 Mar 2011 15:32:47 +0100 |
wenzelm |
statespace syntax: strip positions -- type constraints are unexpected here;
|
file |
diff |
annotate
|
| Sun, 16 Jan 2011 14:57:14 +0100 |
wenzelm |
added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
|
file |
diff |
annotate
|
| Sat, 08 Jan 2011 17:14:48 +0100 |
wenzelm |
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
|
file |
diff |
annotate
|
| Sat, 18 Dec 2010 18:43:13 +0100 |
ballarin |
Add mixins to sublocale command.
|
file |
diff |
annotate
|
| Sun, 05 Sep 2010 21:41:24 +0200 |
wenzelm |
turned show_sorts/show_types into proper configuration options;
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 21:22:07 +0200 |
wenzelm |
eliminated broken Output.no_warnings_CRITICAL -- context visibility does the job;
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 18:36:22 +0200 |
wenzelm |
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 16:08:59 +0200 |
haftmann |
tuned quotes
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 11:02:14 +0200 |
haftmann |
use antiquotations for remaining unqualified constants in HOL
|
file |
diff |
annotate
|
| Thu, 12 Aug 2010 13:28:18 +0200 |
haftmann |
Named_Target.init: empty string represents theory target
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 14:45:38 +0200 |
haftmann |
renamed Theory_Target to the more appropriate Named_Target
|
file |
diff |
annotate
|
| Thu, 27 May 2010 18:10:37 +0200 |
wenzelm |
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
|
file |
diff |
annotate
|
| Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
| Mon, 17 May 2010 15:05:32 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 05 May 2010 18:25:34 +0200 |
haftmann |
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
|
file |
diff |
annotate
|
| Mon, 03 May 2010 14:25:56 +0200 |
wenzelm |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 17:15:23 +0200 |
wenzelm |
adapted ProofContext.infer_type;
|
file |
diff |
annotate
|
| Thu, 15 Apr 2010 15:39:50 +0200 |
wenzelm |
inline old Record.read_typ/cert_typ;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 21:11:15 +0100 |
wenzelm |
modernized structure Local_Theory;
|
file |
diff |
annotate
|
| Tue, 10 Nov 2009 16:04:57 +0100 |
wenzelm |
modernized structure Theory_Target;
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 22:08:47 +0100 |
wenzelm |
adapted LocalTheory.declaration;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 13:15:20 +0100 |
wenzelm |
critical comments;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 15:57:51 +0200 |
wenzelm |
indicate CRITICAL nature of various setmp combinators;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 23:28:10 +0200 |
wenzelm |
replaced String.concat by implode;
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 13:31:38 +0200 |
hoelzl |
Undo errornous commit of Statespace change
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 13:17:17 +0200 |
hoelzl |
correct variable order in approximate-method
|
file |
diff |
annotate
|
| Fri, 28 Aug 2009 21:04:03 +0200 |
wenzelm |
modernized messages -- eliminated ctyp/cterm operations;
|
file |
diff |
annotate
|
| Sat, 25 Jul 2009 18:04:15 +0200 |
wenzelm |
Method.Basic: no position;
|
file |
diff |
annotate
|
| Fri, 19 Jun 2009 17:23:21 +0200 |
haftmann |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 19:58:26 +0100 |
wenzelm |
unified type Proof.method and pervasive METHOD combinators;
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 15:54:58 +0100 |
wenzelm |
Assumption.all_prems_of, Assumption.all_assms_of;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 17:26:14 +0100 |
wenzelm |
moved basic algebra of long names from structure NameSpace to Long_Name;
|
file |
diff |
annotate
|