src/Pure/Isar/theory_target.ML
Wed, 19 Nov 2008 16:58:33 +0100 ballarin Enable switching to new locales during session.
Tue, 18 Nov 2008 09:41:23 +0100 ballarin Code for switching to new locales.
Mon, 17 Nov 2008 17:00:27 +0100 haftmann explicit name morphism function for locale interpretation
Fri, 14 Nov 2008 08:50:11 +0100 haftmann re-educated guess
Thu, 06 Nov 2008 09:09:51 +0100 haftmann cleaned
Tue, 28 Oct 2008 17:53:46 +0100 ballarin Revoked workaround (incompatible with HOL/ex/LocaleTest2.thy).
Mon, 27 Oct 2008 16:20:52 +0100 ballarin Hide path in constant name (workaround).
Mon, 22 Sep 2008 08:00:28 +0200 haftmann temporary workaround for class constants
Wed, 03 Sep 2008 17:47:40 +0200 wenzelm discontinued local axioms -- too difficult to implement, too easy to produce nonsense;
Tue, 02 Sep 2008 22:20:21 +0200 wenzelm tuned;
Tue, 02 Sep 2008 16:55:33 +0200 wenzelm type Attrib.binding abbreviates Name.binding without attributes;
Tue, 02 Sep 2008 14:10:45 +0200 wenzelm explicit type Name.binding for higher-specification elements;
Tue, 29 Jul 2008 08:15:39 +0200 haftmann some steps towards explicit class target for canonical interpretation
Sat, 21 Jun 2008 16:18:52 +0200 wenzelm import_export_proof: simplified thm definition -- PureThy.name_thm does the job;
Sat, 12 Apr 2008 17:00:50 +0200 wenzelm removed unnecessary Goal.close_result;
Mon, 25 Feb 2008 16:31:20 +0100 wenzelm implicit use of LocalTheory.group etc.;
Sun, 10 Feb 2008 20:49:48 +0100 wenzelm tuned spaces;
Sat, 09 Feb 2008 12:56:12 +0100 wenzelm overloading: reduced code redundancy, no xstrings here;
Sat, 26 Jan 2008 17:08:43 +0100 wenzelm grouped versions of axioms/define/notes;
Thu, 24 Jan 2008 23:51:20 +0100 wenzelm replaced ContextPosition by Position.thread_data;
Tue, 08 Jan 2008 11:37:30 +0100 haftmann explicit type variables for instantiation
Mon, 17 Dec 2007 22:40:14 +0100 haftmann note in target
Tue, 11 Dec 2007 10:23:14 +0100 haftmann pretty for instantiation and overloading
Mon, 10 Dec 2007 11:24:15 +0100 haftmann moved instance parameter management from class.ML to axclass.ML
Wed, 05 Dec 2007 14:16:14 +0100 haftmann tuned
Mon, 03 Dec 2007 16:04:17 +0100 haftmann overloading target
Fri, 30 Nov 2007 20:13:08 +0100 haftmann first working version of instance target
Wed, 28 Nov 2007 09:01:42 +0100 haftmann tuned interfaces of class module
Fri, 23 Nov 2007 21:09:35 +0100 haftmann rudimentary instantiation target
Sun, 11 Nov 2007 14:17:15 +0100 wenzelm abbrev: back to PrintMode.internal, which works at least half-way;
Sun, 11 Nov 2007 14:00:11 +0100 wenzelm abbrev: PrintMode.input instead of PrintMode.internal for global version!
Sat, 10 Nov 2007 18:36:10 +0100 wenzelm removed LocalTheory.target_naming/name;
Sat, 10 Nov 2007 14:31:22 +0100 wenzelm locale_const: suppress in class body as well (prevents qualified printing);
Tue, 06 Nov 2007 22:50:38 +0100 wenzelm tuned;
Tue, 06 Nov 2007 13:12:53 +0100 haftmann Class.init now similiar to Locale.init
Mon, 05 Nov 2007 20:50:44 +0100 wenzelm misc cleanup of init functions;
Fri, 02 Nov 2007 18:53:00 +0100 haftmann clarified theory target interface
Tue, 30 Oct 2007 14:39:36 +0100 haftmann clarified
Fri, 26 Oct 2007 22:10:44 +0200 wenzelm locale_const: in_class workaround prevents additional locale version of class consts;
Mon, 22 Oct 2007 21:32:12 +0200 wenzelm tuned;
Mon, 22 Oct 2007 16:54:52 +0200 haftmann tuned abbreviations in class context
Sat, 20 Oct 2007 18:54:34 +0200 wenzelm tuned abbrev interface;
Fri, 19 Oct 2007 20:57:16 +0200 wenzelm internal tuning: class_target, fork_mixfix, declare_const (singleton), abbrev;
Fri, 19 Oct 2007 15:08:33 +0200 haftmann clarified abbreviations in class context
Thu, 18 Oct 2007 16:09:38 +0200 haftmann improved class syntax
Thu, 18 Oct 2007 09:20:59 +0200 haftmann moved fork_mixfix to theory_target
Wed, 17 Oct 2007 13:55:38 +0200 wenzelm tuned fork_mixfix (back from class.ML);
Tue, 16 Oct 2007 23:12:58 +0200 haftmann clarified fork_mixfix
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;
less more (0) -100 -60 tip