| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Sat, 17 Jan 2015 22:52:45 +0100 |
wenzelm |
more compact content for tighter graph layout;
|
file |
diff |
annotate
|
| Thu, 30 Oct 2014 16:20:46 +0100 |
wenzelm |
eliminated aliases;
|
file |
diff |
annotate
|
| Thu, 21 Aug 2014 22:48:39 +0200 |
wenzelm |
tuned signature -- define some elementary operations earlier;
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 23:17:51 +0200 |
wenzelm |
tuned signature -- moved type src to Token, without aliases;
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 12:05:11 +0200 |
wenzelm |
simplified type Proof.method;
|
file |
diff |
annotate
|
| Tue, 05 Aug 2014 16:21:27 +0200 |
wenzelm |
clarified Element.init vs. Element.init' -- the latter also avoids redundant warnings due to declatations when preparing locale expressions / interpretations;
|
file |
diff |
annotate
|
| Sat, 08 Mar 2014 21:08:10 +0100 |
wenzelm |
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
|
file |
diff |
annotate
|
| Wed, 05 Mar 2014 13:11:08 +0100 |
wenzelm |
clarified init_assignable: make double-sure that initial values are reset;
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 10:53:19 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 11 Jan 2014 20:06:31 +0100 |
wenzelm |
check_hyps for attribute application (still inactive, due to non-compliant tools);
|
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
|
| Tue, 30 Jul 2013 15:20:38 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 15:09:25 +0200 |
wenzelm |
type theory is purely value-oriented;
|
file |
diff |
annotate
|
| Sat, 27 Jul 2013 16:35:51 +0200 |
wenzelm |
standardized aliases;
|
file |
diff |
annotate
|
| Thu, 30 May 2013 12:35:40 +0200 |
wenzelm |
standardized aliases;
|
file |
diff |
annotate
|
| Tue, 09 Oct 2012 21:33:12 +0200 |
wenzelm |
clarified Element.init vs. Element.activate: refrain from hard-wiring Thm.def_binding_optional to avoid duplicate facts;
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 22:47:30 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 19:07:32 +0200 |
wenzelm |
added Attrib.global_notes/local_notes/generic_notes convenience;
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 14:17:42 +0100 |
wenzelm |
refined 'interpret': reset facts ("this") and print_result, which merely consist of internal / protected statement;
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 11:23:39 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 10 Mar 2012 17:07:10 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 28 Feb 2012 16:43:32 +0100 |
wenzelm |
display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 17:57:09 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 19 Nov 2011 13:02:50 +0100 |
wenzelm |
do not store vacuous theorem specifications -- relevant for frugal local theory content;
|
file |
diff |
annotate
|
| Mon, 07 Nov 2011 17:00:23 +0100 |
wenzelm |
tuned signature -- avoid spurious Thm.mixed_attribute;
|
file |
diff |
annotate
|
| Sat, 05 Nov 2011 20:40:30 +0100 |
wenzelm |
more uniform instT_subst vs. inst_subst: compare variable names only;
|
file |
diff |
annotate
|
| Sat, 05 Nov 2011 19:47:22 +0100 |
wenzelm |
some performance tuning via Term_Subst/Same.operation;
|
file |
diff |
annotate
|
| Sat, 05 Nov 2011 18:58:40 +0100 |
wenzelm |
pruned signature;
|
file |
diff |
annotate
|
| Thu, 03 Nov 2011 23:32:31 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sat, 29 Oct 2011 00:23:58 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 17:15:52 +0200 |
wenzelm |
tuned signature -- refined terminology;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 15:38:41 +0200 |
wenzelm |
slightly more explicit/syntactic modelling of morphisms;
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 17:23:15 +0200 |
wenzelm |
misc tuning -- eliminated old-fashioned rep_thm;
|
file |
diff |
annotate
|
| Fri, 15 Jul 2011 16:51:01 +0200 |
wenzelm |
Element.activate: leave check of binding where actually applied to the context -- allow internal qualifications, or non-identifier fact names like "assumes *: A" (see also 1183951365de);
|
file |
diff |
annotate
|
| Fri, 15 Jul 2011 00:03:47 +0200 |
wenzelm |
do not check vacous bindings, which routinely occur in locale expressions and long theorem statements etc.;
|
file |
diff |
annotate
|
| Sat, 25 Jun 2011 17:17:49 +0200 |
wenzelm |
clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 21:50:04 +0200 |
wenzelm |
clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 20:58:40 +0200 |
wenzelm |
tuned signature -- eliminated odd comment;
|
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 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 12:46:18 +0200 |
wenzelm |
tuned signature, disentangled dependencies;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 14:20:57 +0200 |
wenzelm |
discontinued special treatment of structure Mixfix;
|
file |
diff |
annotate
|
| Sat, 15 Jan 2011 20:51:22 +0100 |
wenzelm |
clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
|
file |
diff |
annotate
|
| Mon, 03 Jan 2011 14:01:42 +0100 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 17:08:56 +0100 |
wenzelm |
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 16:05:25 +0200 |
wenzelm |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file |
diff |
annotate
|
| Mon, 06 Sep 2010 22:58:06 +0200 |
wenzelm |
turned show_hyps and show_tags into proper configuration option;
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 15:12:49 +0200 |
wenzelm |
structure Thm: less pervasive names;
|
file |
diff |
annotate
|
| Sat, 31 Jul 2010 21:14:20 +0200 |
ballarin |
Interpretation in proofs supports mixins.
|
file |
diff |
annotate
|
| Wed, 05 May 2010 09:24:42 +0200 |
haftmann |
eq_morphism is always optional: avoid trivial morphism for empty list of equations
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 15:52:03 +0200 |
wenzelm |
modernized naming conventions of main Isar proof elements;
|
file |
diff |
annotate
|
| Sat, 13 Mar 2010 20:44:12 +0100 |
wenzelm |
removed unused Args.maxidx_values and Element.generalize_facts;
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:19:47 +0100 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 11:57:16 +0100 |
wenzelm |
modernized structure Local_Defs;
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 20:57:48 +0100 |
wenzelm |
modernized structure Proof_Display;
|
file |
diff |
annotate
|
| Sun, 26 Jul 2009 13:12:54 +0200 |
wenzelm |
Variable.focus: named parameters;
|
file |
diff |
annotate
|
| Sat, 25 Jul 2009 18:04:15 +0200 |
wenzelm |
Method.Basic: no position;
|
file |
diff |
annotate
|