| Thu, 22 Mar 2012 11:11:51 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 21 Mar 2012 21:06:31 +0100 |
wenzelm |
optional 'includes' element for long theorem statements;
|
file |
diff |
annotate
|
| Wed, 21 Mar 2012 17:25:35 +0100 |
wenzelm |
basic support for nested contexts including bundles;
|
file |
diff |
annotate
|
| Mon, 19 Mar 2012 20:32:57 +0100 |
wenzelm |
clarified Binding.name_of vs Name_Space.base_name vs Variable.check_name (see also 9bd8d4addd6e, 3305f573294e);
|
file |
diff |
annotate
|
| Sat, 17 Mar 2012 16:07:03 +0100 |
wenzelm |
refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
|
file |
diff |
annotate
|
| Sat, 17 Mar 2012 13:06:23 +0100 |
wenzelm |
added Syntax.read_typs;
|
file |
diff |
annotate
|
| Sat, 03 Mar 2012 21:52:15 +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
|
| 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
|
| Sun, 20 Nov 2011 17:57:09 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 17:44:41 +0100 |
wenzelm |
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
|
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
|
| Sat, 19 Nov 2011 12:33:18 +0100 |
wenzelm |
put structural attributes of 'obtains' in outer declarations, to make it actually work in local theory;
|
file |
diff |
annotate
|
| Mon, 07 Nov 2011 17:00:23 +0100 |
wenzelm |
tuned signature -- avoid spurious Thm.mixed_attribute;
|
file |
diff |
annotate
|
| Thu, 03 Nov 2011 22:23:41 +0100 |
wenzelm |
tuned signature -- canonical argument order;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2011 22:04:07 +0200 |
wenzelm |
less verbosity in batch mode -- spam reduction and notable performance improvement;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 20:22:22 +0200 |
wenzelm |
tuned signature: Name.invent and Name.invent_names;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 20:58:40 +0200 |
wenzelm |
tuned signature -- eliminated odd comment;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 10:31:18 +0200 |
wenzelm |
more uniform Variable.add_frees/add_fixed etc.;
|
file |
diff |
annotate
|
| Thu, 21 Apr 2011 12:56:27 +0200 |
wenzelm |
discontinuend obsolete Thm.definitionK, which was hardly ever well-defined;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 19:54:04 +0200 |
wenzelm |
report Name_Space.declare/define, relatively to context;
|
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
|
| Wed, 06 Apr 2011 23:17:45 +0200 |
wenzelm |
parallel parsing of big specifications;
|
file |
diff |
annotate
|
| Thu, 24 Mar 2011 16:56:19 +0100 |
wenzelm |
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
|
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
|
| 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
|
| Sun, 12 Sep 2010 19:04:02 +0200 |
wenzelm |
eliminated aliases of Type.constraint;
|
file |
diff |
annotate
|
| Thu, 12 Aug 2010 13:23:46 +0200 |
haftmann |
Named_Target.theory_init
|
file |
diff |
annotate
|