| Mon, 27 Oct 2008 16:20:52 +0100 |
ballarin |
Hide path in constant name (workaround).
|
file |
diff |
annotate
|
| Mon, 22 Sep 2008 08:00:28 +0200 |
haftmann |
temporary workaround for class constants
|
file |
diff |
annotate
|
| Wed, 03 Sep 2008 17:47:40 +0200 |
wenzelm |
discontinued local axioms -- too difficult to implement, too easy to produce nonsense;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 22:20:21 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 16:55:33 +0200 |
wenzelm |
type Attrib.binding abbreviates Name.binding without attributes;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 14:10:45 +0200 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
file |
diff |
annotate
|
| Tue, 29 Jul 2008 08:15:39 +0200 |
haftmann |
some steps towards explicit class target for canonical interpretation
|
file |
diff |
annotate
|
| Sat, 21 Jun 2008 16:18:52 +0200 |
wenzelm |
import_export_proof: simplified thm definition -- PureThy.name_thm does the job;
|
file |
diff |
annotate
|
| Sat, 12 Apr 2008 17:00:50 +0200 |
wenzelm |
removed unnecessary Goal.close_result;
|
file |
diff |
annotate
|
| Mon, 25 Feb 2008 16:31:20 +0100 |
wenzelm |
implicit use of LocalTheory.group etc.;
|
file |
diff |
annotate
|
| Sun, 10 Feb 2008 20:49:48 +0100 |
wenzelm |
tuned spaces;
|
file |
diff |
annotate
|
| Sat, 09 Feb 2008 12:56:12 +0100 |
wenzelm |
overloading: reduced code redundancy, no xstrings here;
|
file |
diff |
annotate
|
| Sat, 26 Jan 2008 17:08:43 +0100 |
wenzelm |
grouped versions of axioms/define/notes;
|
file |
diff |
annotate
|
| Thu, 24 Jan 2008 23:51:20 +0100 |
wenzelm |
replaced ContextPosition by Position.thread_data;
|
file |
diff |
annotate
|
| Tue, 08 Jan 2008 11:37:30 +0100 |
haftmann |
explicit type variables for instantiation
|
file |
diff |
annotate
|
| Mon, 17 Dec 2007 22:40:14 +0100 |
haftmann |
note in target
|
file |
diff |
annotate
|
| Tue, 11 Dec 2007 10:23:14 +0100 |
haftmann |
pretty for instantiation and overloading
|
file |
diff |
annotate
|
| Mon, 10 Dec 2007 11:24:15 +0100 |
haftmann |
moved instance parameter management from class.ML to axclass.ML
|
file |
diff |
annotate
|
| Wed, 05 Dec 2007 14:16:14 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 03 Dec 2007 16:04:17 +0100 |
haftmann |
overloading target
|
file |
diff |
annotate
|
| Fri, 30 Nov 2007 20:13:08 +0100 |
haftmann |
first working version of instance target
|
file |
diff |
annotate
|
| Wed, 28 Nov 2007 09:01:42 +0100 |
haftmann |
tuned interfaces of class module
|
file |
diff |
annotate
|
| Fri, 23 Nov 2007 21:09:35 +0100 |
haftmann |
rudimentary instantiation target
|
file |
diff |
annotate
|
| Sun, 11 Nov 2007 14:17:15 +0100 |
wenzelm |
abbrev: back to PrintMode.internal, which works at least half-way;
|
file |
diff |
annotate
|
| Sun, 11 Nov 2007 14:00:11 +0100 |
wenzelm |
abbrev: PrintMode.input instead of PrintMode.internal for global version!
|
file |
diff |
annotate
|
| Sat, 10 Nov 2007 18:36:10 +0100 |
wenzelm |
removed LocalTheory.target_naming/name;
|
file |
diff |
annotate
|
| Sat, 10 Nov 2007 14:31:22 +0100 |
wenzelm |
locale_const: suppress in class body as well (prevents qualified printing);
|
file |
diff |
annotate
|
| Tue, 06 Nov 2007 22:50:38 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 06 Nov 2007 13:12:53 +0100 |
haftmann |
Class.init now similiar to Locale.init
|
file |
diff |
annotate
|
| Mon, 05 Nov 2007 20:50:44 +0100 |
wenzelm |
misc cleanup of init functions;
|
file |
diff |
annotate
|
| Fri, 02 Nov 2007 18:53:00 +0100 |
haftmann |
clarified theory target interface
|
file |
diff |
annotate
|
| Tue, 30 Oct 2007 14:39:36 +0100 |
haftmann |
clarified
|
file |
diff |
annotate
|
| Fri, 26 Oct 2007 22:10:44 +0200 |
wenzelm |
locale_const: in_class workaround prevents additional locale version of class consts;
|
file |
diff |
annotate
|
| Mon, 22 Oct 2007 21:32:12 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 22 Oct 2007 16:54:52 +0200 |
haftmann |
tuned abbreviations in class context
|
file |
diff |
annotate
|
| Sat, 20 Oct 2007 18:54:34 +0200 |
wenzelm |
tuned abbrev interface;
|
file |
diff |
annotate
|
| Fri, 19 Oct 2007 20:57:16 +0200 |
wenzelm |
internal tuning: class_target, fork_mixfix, declare_const (singleton), abbrev;
|
file |
diff |
annotate
|
| Fri, 19 Oct 2007 15:08:33 +0200 |
haftmann |
clarified abbreviations in class context
|
file |
diff |
annotate
|
| Thu, 18 Oct 2007 16:09:38 +0200 |
haftmann |
improved class syntax
|
file |
diff |
annotate
|
| Thu, 18 Oct 2007 09:20:59 +0200 |
haftmann |
moved fork_mixfix to theory_target
|
file |
diff |
annotate
|
| Wed, 17 Oct 2007 13:55:38 +0200 |
wenzelm |
tuned fork_mixfix (back from class.ML);
|
file |
diff |
annotate
|
| Tue, 16 Oct 2007 23:12:58 +0200 |
haftmann |
clarified fork_mixfix
|
file |
diff |
annotate
|
| Tue, 16 Oct 2007 17:06:19 +0200 |
wenzelm |
misc cleanup of abbrev/local_const;
|
file |
diff |
annotate
|
| Mon, 15 Oct 2007 15:29:46 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sun, 14 Oct 2007 00:18:11 +0200 |
wenzelm |
tuned various Class interfaces;
|
file |
diff |
annotate
|
| Sat, 13 Oct 2007 17:16:45 +0200 |
wenzelm |
abbrev: return hypothetical def;
|
file |
diff |
annotate
|
| Fri, 12 Oct 2007 20:21:58 +0200 |
wenzelm |
pass explicit target record -- more informative peek operation;
|
file |
diff |
annotate
|
| Fri, 12 Oct 2007 14:42:30 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 23:03:11 +0200 |
wenzelm |
local_axioms: impose hyps stemming from local consts as well
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 21:10:43 +0200 |
wenzelm |
local_theory: incorporated consts into axioms;
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 19:10:25 +0200 |
wenzelm |
replaced Term.equiv_types by Type.similar_types;
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 16:05:23 +0200 |
wenzelm |
replaced Sign.add_consts_authentic by Sign.declare_const;
|
file |
diff |
annotate
|
| Wed, 10 Oct 2007 17:31:56 +0200 |
wenzelm |
generalized notation interface (add or del);
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 19:48:55 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 17:10:49 +0200 |
wenzelm |
removed LocalTheory.defs/target_morphism operations;
|
file |
diff |
annotate
|
| Mon, 08 Oct 2007 22:03:21 +0200 |
haftmann |
added proper subclass concept; improved class target
|
file |
diff |
annotate
|
| Mon, 08 Oct 2007 18:13:10 +0200 |
wenzelm |
primitive add_def: strip sorts in axiom;
|
file |
diff |
annotate
|
| Mon, 08 Oct 2007 08:04:28 +0200 |
haftmann |
added first version of user-space type system for class target
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 20:29:24 +0200 |
wenzelm |
replaced literal 'a by Name.aT;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 19:41:52 +0200 |
haftmann |
put declarations first
|
file |
diff |
annotate
|
| Tue, 02 Oct 2007 22:23:31 +0200 |
wenzelm |
added add_defs_new, which strips sorts for axioms (presently inactive);
|
file |
diff |
annotate
|
| Sun, 30 Sep 2007 16:20:41 +0200 |
wenzelm |
keep context position as tags for consts/thms;
|
file |
diff |
annotate
|
| Sat, 29 Sep 2007 08:58:51 +0200 |
haftmann |
proper syntax during class specification
|
file |
diff |
annotate
|
| Thu, 20 Sep 2007 16:37:29 +0200 |
haftmann |
fixed wrong syntax treatment in class target
|
file |
diff |
annotate
|
| Tue, 21 Aug 2007 20:05:40 +0200 |
wenzelm |
ProofContext.restore_mode;
|
file |
diff |
annotate
|
| Fri, 17 Aug 2007 13:58:57 +0200 |
haftmann |
dropped junk
|
file |
diff |
annotate
|
| Fri, 10 Aug 2007 17:04:24 +0200 |
haftmann |
ClassPackage renamed to Class
|
file |
diff |
annotate
|
| Sat, 02 Jun 2007 18:05:34 +0200 |
wenzelm |
added target/local_abbrev (from proof_context.ML);
|
file |
diff |
annotate
|
| Thu, 24 May 2007 08:37:39 +0200 |
haftmann |
rudimentary class target implementation
|
file |
diff |
annotate
|
| Mon, 07 May 2007 00:49:59 +0200 |
wenzelm |
simplified DataFun interfaces;
|
file |
diff |
annotate
|
| Sun, 15 Apr 2007 14:31:49 +0200 |
wenzelm |
proper ProofContext.infer_types;
|
file |
diff |
annotate
|
| Sat, 14 Apr 2007 00:46:23 +0200 |
wenzelm |
declarations: apply target_morphism;
|
file |
diff |
annotate
|
| Fri, 09 Mar 2007 08:45:55 +0100 |
haftmann |
*** empty log message ***
|
file |
diff |
annotate
|
| Wed, 28 Feb 2007 22:05:46 +0100 |
wenzelm |
abbrev: be permissive after transformation;
|
file |
diff |
annotate
|
| Fri, 23 Feb 2007 08:39:26 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sat, 10 Feb 2007 09:26:20 +0100 |
haftmann |
added class target stub
|
file |
diff |
annotate
|
| Sun, 28 Jan 2007 23:29:17 +0100 |
wenzelm |
added interface for target_naming;
|
file |
diff |
annotate
|
| Thu, 14 Dec 2006 15:31:22 +0100 |
wenzelm |
defs/notes: more robust transitivity reasoning;
|
file |
diff |
annotate
|
| Wed, 13 Dec 2006 15:47:36 +0100 |
wenzelm |
internal_abbrev: observe print mode;
|
file |
diff |
annotate
|
| Tue, 12 Dec 2006 21:25:14 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 12 Dec 2006 20:49:31 +0100 |
wenzelm |
removed is_class -- handled internally;
|
file |
diff |
annotate
|
| Sun, 10 Dec 2006 22:27:03 +0100 |
wenzelm |
defs: increased entropy of mixfix handling;
|
file |
diff |
annotate
|
| Sun, 10 Dec 2006 17:37:55 +0100 |
wenzelm |
removed junk;
|
file |
diff |
annotate
|
| Sun, 10 Dec 2006 15:30:46 +0100 |
wenzelm |
added is_class (approximation);
|
file |
diff |
annotate
|
| Sat, 09 Dec 2006 18:05:37 +0100 |
wenzelm |
TermSyntax.abbrev;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2006 23:16:55 +0100 |
wenzelm |
reorganized structure Tactic vs. MetaSimplifier;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2006 17:58:39 +0100 |
wenzelm |
TermSyntax.notation/abbrevs;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 22:14:53 +0100 |
wenzelm |
target_name: allow qualified names;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 00:29:16 +0100 |
wenzelm |
notes: added non-official name;
|
file |
diff |
annotate
|
| Thu, 30 Nov 2006 17:42:23 +0100 |
wenzelm |
notes: proper naming of thm proof, activated import_export_proof;
|
file |
diff |
annotate
|
| Thu, 30 Nov 2006 16:48:42 +0100 |
wenzelm |
notes: more careful treatment of Goal.close_result;
|
file |
diff |
annotate
|
| Thu, 30 Nov 2006 14:17:37 +0100 |
wenzelm |
notes: proper import/export of proofs (still inactive);
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 15:45:02 +0100 |
wenzelm |
reworked notes: towards proper import/export of proof terms;
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 04:11:18 +0100 |
wenzelm |
Assumption.assms_of: cterm;
|
file |
diff |
annotate
|
| Tue, 28 Nov 2006 00:35:27 +0100 |
wenzelm |
simplified '?' operator;
|
file |
diff |
annotate
|
| Sun, 26 Nov 2006 18:07:31 +0100 |
wenzelm |
simplified consts: no auxiliary params, sane mixfix syntax;
|
file |
diff |
annotate
|
| Thu, 23 Nov 2006 20:33:37 +0100 |
wenzelm |
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
|
file |
diff |
annotate
|
| Wed, 22 Nov 2006 17:38:36 +0100 |
wenzelm |
consts: ProofContext.set_stmt true -- avoids naming of local thms;
|
file |
diff |
annotate
|
| Tue, 21 Nov 2006 18:07:29 +0100 |
wenzelm |
LocalTheory.axioms/notes/defs: proper kind;
|
file |
diff |
annotate
|
| Fri, 10 Nov 2006 22:18:53 +0100 |
wenzelm |
removed mapping;
|
file |
diff |
annotate
|
| Thu, 09 Nov 2006 21:44:34 +0100 |
wenzelm |
init: '-' refers to global context;
|
file |
diff |
annotate
|
| Sat, 14 Oct 2006 23:25:56 +0200 |
wenzelm |
added peek;
|
file |
diff |
annotate
|
| Thu, 12 Oct 2006 22:57:42 +0200 |
wenzelm |
added peek;
|
file |
diff |
annotate
|
| Wed, 11 Oct 2006 22:55:21 +0200 |
wenzelm |
exit: pass interactive flag;
|
file |
diff |
annotate
|
| Wed, 11 Oct 2006 00:27:37 +0200 |
wenzelm |
added begin;
|
file |
diff |
annotate
|
| Mon, 09 Oct 2006 02:20:08 +0200 |
wenzelm |
added exit;
|
file |
diff |
annotate
|
| Sat, 07 Oct 2006 01:31:23 +0200 |
wenzelm |
Common theory targets.
|
file |
diff |
annotate
|