src/Pure/Isar/class_target.ML
Sat, 31 Jul 2010 21:14:20 +0200 ballarin Make registrations generic data.
Thu, 01 Jul 2010 16:54:44 +0200 haftmann "prod" and "sum" replace "*" and "+" respectively
Thu, 10 Jun 2010 12:26:07 +0200 haftmann adjust popular symbolic type constructors
Tue, 01 Jun 2010 15:59:01 +0200 haftmann do not expose store flag of AxClass.add_*
Tue, 01 Jun 2010 11:30:57 +0200 berghofe merged
Tue, 01 Jun 2010 11:04:49 +0200 berghofe classrel and arity theorems are now stored under proper name in theory. add_arity and
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;
Thu, 27 May 2010 17:41:27 +0200 wenzelm renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
Wed, 05 May 2010 09:24:42 +0200 haftmann eq_morphism is always optional: avoid trivial morphism for empty list of equations
Wed, 05 May 2010 08:57:23 +0200 haftmann tuned interpunctation, dropped dead comment
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;
Wed, 28 Apr 2010 13:30:17 +0200 haftmann codified comment
Sun, 25 Apr 2010 21:18:04 +0200 wenzelm replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
Sun, 25 Apr 2010 15:52:03 +0200 wenzelm modernized naming conventions of main Isar proof elements;
Sun, 11 Apr 2010 14:30:34 +0200 wenzelm Thm.add_axiom/add_def: return internal name of foundational axiom;
Sun, 21 Mar 2010 08:46:49 +0100 haftmann handle hidden polymorphism in class target (without class target syntax, though)
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;
Tue, 09 Mar 2010 14:35:02 +0100 wenzelm added ProofContext.tsig_of -- proforma version for local name space only, not logical content;
Tue, 23 Feb 2010 10:11:12 +0100 haftmann dropped axclass
Mon, 15 Feb 2010 14:04:06 +0100 haftmann clarifed type
Sun, 07 Feb 2010 19:33:34 +0100 wenzelm renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
Mon, 30 Nov 2009 12:28:12 +0100 haftmann dropped some unused bindings
Mon, 30 Nov 2009 11:42:48 +0100 haftmann more accurate linerarity
Fri, 13 Nov 2009 21:11:15 +0100 wenzelm modernized structure Local_Theory;
Sun, 08 Nov 2009 18:43:42 +0100 wenzelm adapted Theory_Data;
Sun, 08 Nov 2009 16:30:41 +0100 wenzelm adapted Generic_Data, Proof_Data;
Sun, 25 Oct 2009 21:35:46 +0100 wenzelm eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
Sat, 17 Oct 2009 16:58:03 +0200 wenzelm operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
Sat, 17 Oct 2009 15:57:51 +0200 wenzelm indicate CRITICAL nature of various setmp combinators;
Thu, 01 Oct 2009 17:11:48 +0200 haftmann proper merge of interpretation equations
Thu, 01 Oct 2009 07:40:25 +0200 ballarin Merged.
Wed, 19 Aug 2009 19:35:46 +0200 ballarin Improved comments and api names.
Sat, 15 Aug 2009 15:29:54 +0200 haftmann additional checkpoints avoid problems in error situations
Wed, 15 Jul 2009 18:20:08 +0200 haftmann simplification of locale interfaces
Fri, 10 Jul 2009 07:59:29 +0200 haftmann tuned locale interface
Mon, 29 Jun 2009 16:17:57 +0200 haftmann mutual instances
Wed, 17 Jun 2009 17:42:41 +0200 haftmann stripped dead comment
Sun, 14 Jun 2009 17:20:19 +0200 haftmann axclass command now legacy
Tue, 09 Jun 2009 22:59:55 +0200 haftmann tuned make/map/merge combinators
Sun, 24 May 2009 15:02:22 +0200 haftmann tuned class user space type system code
Wed, 20 May 2009 15:35:13 +0200 haftmann tuned
Wed, 20 May 2009 12:09:07 +0200 haftmann avoid potential problem with stale theory
Tue, 28 Apr 2009 13:34:48 +0200 haftmann prevent potential failure
Sat, 28 Mar 2009 20:25:23 +0100 wenzelm simplified Locale.activate operations, using generic context;
Fri, 13 Mar 2009 23:56:07 +0100 wenzelm merged
Fri, 13 Mar 2009 19:17:58 +0100 haftmann coherent binding policy with primitive target operations
Fri, 13 Mar 2009 23:50:05 +0100 wenzelm simplified method setup;
Fri, 13 Mar 2009 19:58:26 +0100 wenzelm unified type Proof.method and pervasive METHOD combinators;
Sun, 08 Mar 2009 17:26:14 +0100 wenzelm moved basic algebra of long names from structure NameSpace to Long_Name;
Sat, 07 Mar 2009 22:16:50 +0100 wenzelm more uniform handling of binding in targets and derived elements;
Thu, 05 Mar 2009 12:08:00 +0100 wenzelm renamed NameSpace.base to NameSpace.base_name;
Wed, 18 Feb 2009 19:18:32 +0100 haftmann more precise improvement in instantiation user space type system
Mon, 26 Jan 2009 22:14:19 +0100 haftmann fixed reading of class specs: declare class operations in context
Wed, 21 Jan 2009 23:40:23 +0100 haftmann allow empty class specs
Wed, 21 Jan 2009 16:47:03 +0100 haftmann code cleanup
Mon, 19 Jan 2009 08:16:42 +0100 haftmann improved tackling of subclasses
Sat, 17 Jan 2009 22:07:29 +0100 haftmann tuned signature
Sat, 17 Jan 2009 08:29:54 +0100 haftmann code cleanup
Fri, 16 Jan 2009 14:58:11 +0100 haftmann migrated class package to new locale implementation
Sun, 11 Jan 2009 14:18:16 +0100 haftmann construct explicit class morphism
less more (0) -60 tip