Wed, 11 Aug 2010 12:24:24 +0200 |
haftmann |
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
|
file |
diff |
annotate
|
Wed, 11 Aug 2010 08:59:41 +0200 |
haftmann |
whitespace tuning
|
file |
diff |
annotate
|
Wed, 11 Aug 2010 08:58:18 +0200 |
haftmann |
remove overloading and instantiation from data slot
|
file |
diff |
annotate
|
Tue, 10 Aug 2010 16:03:54 +0200 |
haftmann |
separate initialisation for overloading and instantiation target
|
file |
diff |
annotate
|
Tue, 10 Aug 2010 15:38:33 +0200 |
haftmann |
different foundations for different targets; simplified syntax handling of abbreviations
|
file |
diff |
annotate
|
Tue, 10 Aug 2010 15:07:39 +0200 |
haftmann |
avoiding redundant primes
|
file |
diff |
annotate
|
Tue, 10 Aug 2010 14:57:58 +0200 |
haftmann |
separated type from term parameters
|
file |
diff |
annotate
|
Tue, 10 Aug 2010 14:53:41 +0200 |
haftmann |
moved extra_tfrees check for mixfix syntax to Generic_Target
|
file |
diff |
annotate
|
Tue, 10 Aug 2010 14:47:22 +0200 |
haftmann |
name and argument grouping tuning
|
file |
diff |
annotate
|
Tue, 10 Aug 2010 14:42:30 +0200 |
haftmann |
whitespace tuning
|
file |
diff |
annotate
|
Tue, 10 Aug 2010 14:11:28 +0200 |
haftmann |
try to uniformly follow define/note/abbrev/declaration order as close as possible
|
file |
diff |
annotate
|
Tue, 10 Aug 2010 14:06:38 +0200 |
haftmann |
split off structure Generic_Target into separate file
|
file |
diff |
annotate
|
Tue, 10 Aug 2010 13:58:26 +0200 |
haftmann |
split off generic parts of target implementations into separate structure
|
file |
diff |
annotate
|
Tue, 10 Aug 2010 13:25:33 +0200 |
haftmann |
restructured code for `declaration`
|
file |
diff |
annotate
|
Mon, 09 Aug 2010 16:56:00 +0200 |
haftmann |
factored out foundation of `define` into separate function
|
file |
diff |
annotate
|
Mon, 09 Aug 2010 16:30:23 +0200 |
haftmann |
combine declaration and definition of foundation constant
|
file |
diff |
annotate
|
Mon, 09 Aug 2010 15:51:27 +0200 |
haftmann |
more appropriate outline of `define`
|
file |
diff |
annotate
|
Mon, 09 Aug 2010 15:43:37 +0200 |
haftmann |
backlink definition to target `notes`
|
file |
diff |
annotate
|
Mon, 09 Aug 2010 15:38:46 +0200 |
haftmann |
dropped idle local_facts argument; factored out theory_abbrev and locale_abbrev
|
file |
diff |
annotate
|
Mon, 09 Aug 2010 15:20:50 +0200 |
haftmann |
more convenient order
|
file |
diff |
annotate
|
Mon, 09 Aug 2010 15:19:45 +0200 |
haftmann |
dropped misleading comments
|
file |
diff |
annotate
|
Mon, 09 Aug 2010 14:47:28 +0200 |
haftmann |
separated foundation of `notes`
|
file |
diff |
annotate
|
Mon, 09 Aug 2010 14:20:21 +0200 |
haftmann |
more clear separation into local and global facts
|
file |
diff |
annotate
|
Mon, 09 Aug 2010 14:07:23 +0200 |
haftmann |
sharpened and tuned educated guess for canonical class morphism
|
file |
diff |
annotate
|
Sun, 08 Aug 2010 20:51:02 +0200 |
haftmann |
discontinued separation of `define` and `declare_const`
|
file |
diff |
annotate
|
Sun, 08 Aug 2010 20:41:25 +0200 |
haftmann |
unravelled target initialization code
|
file |
diff |
annotate
|
Fri, 04 Jun 2010 15:48:13 +0200 |
wenzelm |
more robust handling of additional type variables: warning, more canonical order, drop mixfix syntax if implicit type arguments are introduced (to avoid delusion due to shifted arguments);
|
file |
diff |
annotate
|
Mon, 31 May 2010 10:27:42 +0200 |
wenzelm |
Theory_Target.pretty: more markup;
|
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, 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
|
Sun, 11 Apr 2010 14:30:34 +0200 |
wenzelm |
Thm.add_axiom/add_def: return internal name of foundational axiom;
|
file |
diff |
annotate
|
Sun, 21 Mar 2010 08:46:49 +0100 |
haftmann |
handle hidden polymorphism in class target (without class target syntax, though)
|
file |
diff |
annotate
|
Sat, 20 Mar 2010 17:33:11 +0100 |
wenzelm |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
file |
diff |
annotate
|
Mon, 15 Mar 2010 18:59:16 +0100 |
wenzelm |
replaced type_syntax/term_syntax by uniform syntax_declaration;
|
file |
diff |
annotate
|
Sat, 13 Mar 2010 20:33:14 +0100 |
wenzelm |
local theory specifications handle hidden polymorphism implicitly;
|
file |
diff |
annotate
|
Sat, 13 Mar 2010 19:35:53 +0100 |
wenzelm |
minor tuning and simplification;
|
file |
diff |
annotate
|
Sat, 13 Mar 2010 14:41:14 +0100 |
wenzelm |
Local_Defs.contract convenience;
|
file |
diff |
annotate
|
Thu, 11 Mar 2010 23:45:41 +0100 |
wenzelm |
more basic Local_Defs.export_cterm;
|
file |
diff |
annotate
|
Sun, 07 Mar 2010 11:57:16 +0100 |
wenzelm |
modernized structure Local_Defs;
|
file |
diff |
annotate
|
Thu, 18 Feb 2010 23:41:01 +0100 |
wenzelm |
removed unused Theory_Target.begin;
|
file |
diff |
annotate
|
Mon, 15 Feb 2010 14:04:06 +0100 |
haftmann |
apply global morphism for theory, instantiation and overloading target; n.b. target morphism and global morphism coincide for theory target
|
file |
diff |
annotate
|
Thu, 19 Nov 2009 14:44:22 +0100 |
wenzelm |
Local_Theory.define: eliminated slightly odd kind argument -- such low-level definitions should be hardly ever exposed to end-users anyway;
|
file |
diff |
annotate
|
Tue, 17 Nov 2009 14:50:55 +0100 |
wenzelm |
uniform new_group/reset_group;
|
file |
diff |
annotate
|
Sun, 15 Nov 2009 19:45:05 +0100 |
wenzelm |
eliminated obsolete thm position tags;
|
file |
diff |
annotate
|
Fri, 13 Nov 2009 21:11:15 +0100 |
wenzelm |
modernized structure Local_Theory;
|
file |
diff |
annotate
|
Fri, 13 Nov 2009 20:41:29 +0100 |
wenzelm |
eliminated slightly odd kind argument of LocalTheory.note(s);
|
file |
diff |
annotate
|
Tue, 10 Nov 2009 16:04:57 +0100 |
wenzelm |
modernized structure Theory_Target;
|
file |
diff |
annotate
|
Mon, 09 Nov 2009 20:47:39 +0100 |
wenzelm |
locale_const/target_notation: uniform use of Term.aconv_untyped;
|
file |
diff |
annotate
|
Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
Fri, 06 Nov 2009 10:26:13 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
Wed, 04 Nov 2009 22:54:42 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
|
Mon, 02 Nov 2009 21:27:26 +0100 |
ballarin |
Relax on type agreement with original context when applying term syntax.
|
file |
diff |
annotate
|
Thu, 05 Nov 2009 22:06:46 +0100 |
wenzelm |
allow "pervasive" local theory declarations, which are applied the background theory;
|
file |
diff |
annotate
|
Wed, 28 Oct 2009 17:38:13 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
Sun, 25 Oct 2009 21:35:46 +0100 |
wenzelm |
eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
|
file |
diff |
annotate
|
Sun, 25 Oct 2009 19:18:59 +0100 |
wenzelm |
maintain group via name space, not tags;
|
file |
diff |
annotate
|
Wed, 30 Sep 2009 22:24:57 +0200 |
wenzelm |
eliminated redundant parameters;
|
file |
diff |
annotate
|
Wed, 15 Jul 2009 23:11:57 +0200 |
wenzelm |
eliminated obsolete legacy_varify;
|
file |
diff |
annotate
|
Thu, 09 Jul 2009 22:48:12 +0200 |
wenzelm |
renamed structure TermSubst to Term_Subst;
|
file |
diff |
annotate
|
Mon, 29 Jun 2009 16:17:57 +0200 |
haftmann |
mutual instances
|
file |
diff |
annotate
|