| Thu, 13 Aug 2015 11:05:19 +0200 |
wenzelm |
tuned signature, in accordance to sortBy in Scala;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 16:35:12 +0200 |
wenzelm |
tuned signature for print_nested_cases;
|
file |
diff |
annotate
|
| Thu, 02 Jul 2015 12:33:04 +0200 |
wenzelm |
allow to specify suffix of goal parameters;
|
file |
diff |
annotate
|
| Thu, 25 Jun 2015 23:49:05 +0200 |
wenzelm |
implicit goal cases are legacy;
|
file |
diff |
annotate
|
| Thu, 25 Jun 2015 12:10:07 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 24 Jun 2015 21:26:03 +0200 |
wenzelm |
clarified 'case' command;
|
file |
diff |
annotate
|
| Mon, 15 Jun 2015 16:59:27 +0200 |
wenzelm |
vacuous fact `TERM x`;
|
file |
diff |
annotate
|
| Sun, 14 Jun 2015 15:53:13 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 14 Jun 2015 14:59:39 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 10 Jun 2015 11:52:54 +0200 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Tue, 09 Jun 2015 22:24:33 +0200 |
wenzelm |
more uniform treatment of auto bindings vs. explicit user bindings;
|
file |
diff |
annotate
|
| Tue, 09 Jun 2015 16:42:17 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 09 Jun 2015 11:51:05 +0200 |
wenzelm |
clarified term bindings;
|
file |
diff |
annotate
|
| Mon, 08 Jun 2015 20:53:42 +0200 |
wenzelm |
clarified Proof_Context.cert_propp/read_propp;
|
file |
diff |
annotate
|
| Mon, 08 Jun 2015 19:38:08 +0200 |
wenzelm |
more careful treatment of term bindings in 'obtain' proof body;
|
file |
diff |
annotate
|
| Mon, 08 Jun 2015 14:45:31 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 07 Jun 2015 23:37:32 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 07 Jun 2015 22:04:50 +0200 |
wenzelm |
tuned (see also 66e6c539a36d);
|
file |
diff |
annotate
|
| Sun, 07 Jun 2015 21:58:18 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 07 Jun 2015 21:30:53 +0200 |
wenzelm |
clarified: declare props once and for all;
|
file |
diff |
annotate
|
| Sun, 07 Jun 2015 20:03:40 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 07 Jun 2015 15:01:07 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 03 Jun 2015 19:25:05 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Sun, 03 May 2015 17:19:27 +0200 |
wenzelm |
tuned output -- avoid empty quites and extra breaks;
|
file |
diff |
annotate
|
| Thu, 09 Apr 2015 20:42:32 +0200 |
wenzelm |
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 19:39:08 +0200 |
wenzelm |
proper context for Object_Logic operations;
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 22:11:01 +0200 |
wenzelm |
support for 'restricted' modifier: only qualified accesses outside the local scope;
|
file |
diff |
annotate
|
| Sat, 04 Apr 2015 14:04:11 +0200 |
wenzelm |
support private scope for individual local theory commands;
|
file |
diff |
annotate
|
| Fri, 03 Apr 2015 19:56:51 +0200 |
wenzelm |
more uniform "verbose" option to print name space;
|
file |
diff |
annotate
|
| Wed, 01 Apr 2015 18:17:44 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 22:31:05 +0200 |
wenzelm |
support for explicit scope of private entries;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 17:34:52 +0200 |
wenzelm |
clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 00:11:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 29 Mar 2015 19:23:08 +0200 |
wenzelm |
proper local Proof_Context.arity_sorts;
|
file |
diff |
annotate
|
| Tue, 24 Mar 2015 11:53:18 +0100 |
wenzelm |
clarified input source;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 13:28:04 +0100 |
wenzelm |
tuned -- more explicit use of context;
|
file |
diff |
annotate
|
| Sun, 01 Mar 2015 23:35:41 +0100 |
wenzelm |
added Proof_Context.cterm_of/ctyp_of convenience;
|
file |
diff |
annotate
|
| Fri, 19 Dec 2014 17:23:56 +0100 |
wenzelm |
more frugal Local_Syntax.init -- maintain idents within context;
|
file |
diff |
annotate
|
| Sun, 30 Nov 2014 13:15:04 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 30 Nov 2014 12:24:56 +0100 |
wenzelm |
more abstract type Input.source;
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Sat, 08 Nov 2014 21:31:51 +0100 |
wenzelm |
optional proof context for unify operations, for the sake of proper local options;
|
file |
diff |
annotate
|
| Mon, 13 Oct 2014 22:43:29 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 20 Aug 2014 11:51:39 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 16:20:14 +0200 |
wenzelm |
more informative Token.Fact: retain name of dynamic fact (without selection);
|
file |
diff |
annotate
|
| Wed, 13 Aug 2014 14:57:03 +0200 |
wenzelm |
transfer result of Global_Theory.add_thms_dynamic to context stack;
|
file |
diff |
annotate
|
| Sun, 10 Aug 2014 19:44:20 +0200 |
wenzelm |
support aliases within the facts space;
|
file |
diff |
annotate
|
| Wed, 02 Jul 2014 12:12:26 +0200 |
wenzelm |
check 'case' variable bindings as for 'fix', which means internal names are rejected as usual;
|
file |
diff |
annotate
|
| Fri, 27 Jun 2014 16:04:56 +0200 |
wenzelm |
command 'print_term_bindings' supersedes 'print_binds';
|
file |
diff |
annotate
|
| Mon, 05 May 2014 16:30:19 +0200 |
wenzelm |
more print operations;
|
file |
diff |
annotate
|
| Mon, 05 May 2014 15:17:07 +0200 |
wenzelm |
support print operations as asynchronous query;
|
file |
diff |
annotate
|
| Sun, 06 Apr 2014 16:36:28 +0200 |
wenzelm |
more source positions;
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 12:35:39 +0200 |
wenzelm |
some shortcuts for chunks, which sometimes avoid bulky string output;
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 10:28:08 +0200 |
wenzelm |
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
|
file |
diff |
annotate
|
| Wed, 26 Mar 2014 14:41:52 +0100 |
wenzelm |
prefer Context_Position where a context is available;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 12:25:17 +0100 |
wenzelm |
more markup for improper elements;
|
file |
diff |
annotate
|
| Sat, 15 Mar 2014 11:22:25 +0100 |
wenzelm |
more explicit treatment of verbose mode, which includes concealed entries;
|
file |
diff |
annotate
|
| Sat, 15 Mar 2014 10:24:49 +0100 |
wenzelm |
clarified retrieve_generic: local error takes precedence, which is relevant for completion;
|
file |
diff |
annotate
|
| Sat, 15 Mar 2014 10:14:42 +0100 |
wenzelm |
clarified print_local_facts;
|
file |
diff |
annotate
|