| Wed, 27 Apr 2016 10:03:35 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 26 Apr 2016 16:20:28 +0200 |
wenzelm |
defs are closed, which leads to proper auto_bind_facts;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2015 14:11:54 +0100 |
wenzelm |
avoid vacuous quantification, as usual for shared variable scope;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2015 11:41:11 +0100 |
wenzelm |
support for structure statements in 'assume', 'presume';
|
file |
diff |
annotate
|
| Thu, 09 Jul 2015 22:08:20 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sat, 13 Jun 2015 16:35:27 +0200 |
wenzelm |
eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
|
file |
diff |
annotate
|
| Mon, 23 Mar 2015 19:43:03 +0100 |
wenzelm |
local fixes may depend on goal params;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 15:12:03 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 12:34:50 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 17:47:23 +0200 |
wenzelm |
clarified defer/prefer: more specific errors;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 20:05:58 +0100 |
wenzelm |
renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 19:06:05 +0100 |
wenzelm |
renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 17:45:04 +0100 |
wenzelm |
discontinued old-style Term.list_all_free in favour of plain Logic.all;
|
file |
diff |
annotate
|
| Sat, 05 Nov 2011 15:00:49 +0100 |
wenzelm |
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
|
file |
diff |
annotate
|