src/Pure/Isar/theory_target.ML
Tue, 16 Oct 2007 17:06:19 +0200 wenzelm misc cleanup of abbrev/local_const;
Mon, 15 Oct 2007 15:29:46 +0200 haftmann tuned
Sun, 14 Oct 2007 00:18:11 +0200 wenzelm tuned various Class interfaces;
Sat, 13 Oct 2007 17:16:45 +0200 wenzelm abbrev: return hypothetical def;
Fri, 12 Oct 2007 20:21:58 +0200 wenzelm pass explicit target record -- more informative peek operation;
Fri, 12 Oct 2007 14:42:30 +0200 haftmann tuned
Thu, 11 Oct 2007 23:03:11 +0200 wenzelm local_axioms: impose hyps stemming from local consts as well
Thu, 11 Oct 2007 21:10:43 +0200 wenzelm local_theory: incorporated consts into axioms;
Thu, 11 Oct 2007 19:10:25 +0200 wenzelm replaced Term.equiv_types by Type.similar_types;
Thu, 11 Oct 2007 16:05:23 +0200 wenzelm replaced Sign.add_consts_authentic by Sign.declare_const;
Wed, 10 Oct 2007 17:31:56 +0200 wenzelm generalized notation interface (add or del);
Tue, 09 Oct 2007 19:48:55 +0200 wenzelm tuned;
Tue, 09 Oct 2007 17:10:49 +0200 wenzelm removed LocalTheory.defs/target_morphism operations;
Mon, 08 Oct 2007 22:03:21 +0200 haftmann added proper subclass concept; improved class target
Mon, 08 Oct 2007 18:13:10 +0200 wenzelm primitive add_def: strip sorts in axiom;
Mon, 08 Oct 2007 08:04:28 +0200 haftmann added first version of user-space type system for class target
Thu, 04 Oct 2007 20:29:24 +0200 wenzelm replaced literal 'a by Name.aT;
Thu, 04 Oct 2007 19:41:52 +0200 haftmann put declarations first
Tue, 02 Oct 2007 22:23:31 +0200 wenzelm added add_defs_new, which strips sorts for axioms (presently inactive);
Sun, 30 Sep 2007 16:20:41 +0200 wenzelm keep context position as tags for consts/thms;
Sat, 29 Sep 2007 08:58:51 +0200 haftmann proper syntax during class specification
Thu, 20 Sep 2007 16:37:29 +0200 haftmann fixed wrong syntax treatment in class target
Tue, 21 Aug 2007 20:05:40 +0200 wenzelm ProofContext.restore_mode;
Fri, 17 Aug 2007 13:58:57 +0200 haftmann dropped junk
Fri, 10 Aug 2007 17:04:24 +0200 haftmann ClassPackage renamed to Class
Sat, 02 Jun 2007 18:05:34 +0200 wenzelm added target/local_abbrev (from proof_context.ML);
Thu, 24 May 2007 08:37:39 +0200 haftmann rudimentary class target implementation
Mon, 07 May 2007 00:49:59 +0200 wenzelm simplified DataFun interfaces;
Sun, 15 Apr 2007 14:31:49 +0200 wenzelm proper ProofContext.infer_types;
Sat, 14 Apr 2007 00:46:23 +0200 wenzelm declarations: apply target_morphism;
Fri, 09 Mar 2007 08:45:55 +0100 haftmann *** empty log message ***
Wed, 28 Feb 2007 22:05:46 +0100 wenzelm abbrev: be permissive after transformation;
Fri, 23 Feb 2007 08:39:26 +0100 haftmann tuned
Sat, 10 Feb 2007 09:26:20 +0100 haftmann added class target stub
Sun, 28 Jan 2007 23:29:17 +0100 wenzelm added interface for target_naming;
Thu, 14 Dec 2006 15:31:22 +0100 wenzelm defs/notes: more robust transitivity reasoning;
Wed, 13 Dec 2006 15:47:36 +0100 wenzelm internal_abbrev: observe print mode;
Tue, 12 Dec 2006 21:25:14 +0100 wenzelm tuned;
Tue, 12 Dec 2006 20:49:31 +0100 wenzelm removed is_class -- handled internally;
Sun, 10 Dec 2006 22:27:03 +0100 wenzelm defs: increased entropy of mixfix handling;
Sun, 10 Dec 2006 17:37:55 +0100 wenzelm removed junk;
Sun, 10 Dec 2006 15:30:46 +0100 wenzelm added is_class (approximation);
Sat, 09 Dec 2006 18:05:37 +0100 wenzelm TermSyntax.abbrev;
Thu, 07 Dec 2006 23:16:55 +0100 wenzelm reorganized structure Tactic vs. MetaSimplifier;
Thu, 07 Dec 2006 17:58:39 +0100 wenzelm TermSyntax.notation/abbrevs;
Tue, 05 Dec 2006 22:14:53 +0100 wenzelm target_name: allow qualified names;
Tue, 05 Dec 2006 00:29:16 +0100 wenzelm notes: added non-official name;
Thu, 30 Nov 2006 17:42:23 +0100 wenzelm notes: proper naming of thm proof, activated import_export_proof;
Thu, 30 Nov 2006 16:48:42 +0100 wenzelm notes: more careful treatment of Goal.close_result;
Thu, 30 Nov 2006 14:17:37 +0100 wenzelm notes: proper import/export of proofs (still inactive);
Wed, 29 Nov 2006 15:45:02 +0100 wenzelm reworked notes: towards proper import/export of proof terms;
Wed, 29 Nov 2006 04:11:18 +0100 wenzelm Assumption.assms_of: cterm;
Tue, 28 Nov 2006 00:35:27 +0100 wenzelm simplified '?' operator;
Sun, 26 Nov 2006 18:07:31 +0100 wenzelm simplified consts: no auxiliary params, sane mixfix syntax;
Thu, 23 Nov 2006 20:33:37 +0100 wenzelm uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
Wed, 22 Nov 2006 17:38:36 +0100 wenzelm consts: ProofContext.set_stmt true -- avoids naming of local thms;
Tue, 21 Nov 2006 18:07:29 +0100 wenzelm LocalTheory.axioms/notes/defs: proper kind;
Fri, 10 Nov 2006 22:18:53 +0100 wenzelm removed mapping;
Thu, 09 Nov 2006 21:44:34 +0100 wenzelm init: '-' refers to global context;
Sat, 14 Oct 2006 23:25:56 +0200 wenzelm added peek;
less more (0) -60 tip