src/Pure/Isar/class.ML
Sat, 31 Jul 2010 21:14:20 +0200 ballarin Make registrations generic data.
Mon, 24 May 2010 10:48:32 +0200 ballarin Reapply mixin patch: base for performance improvements.
Fri, 14 May 2010 21:23:29 +0200 ballarin Revert mixin patch due to inacceptable performance drop.
Thu, 13 May 2010 13:29:43 +0200 ballarin Remove improper use of mixin in class package.
Sat, 08 May 2010 19:18:28 +0200 wenzelm tuned error message: regular Pretty.string_of instead of raw Pretty.output;
Sat, 08 May 2010 19:14:13 +0200 wenzelm unified/simplified Pretty.margin_default;
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
Tue, 04 May 2010 14:44:30 +0200 wenzelm merged
Tue, 04 May 2010 08:55:43 +0200 haftmann locale predicates of classes carry a mandatory "class" prefix
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:52 +0200 haftmann merged
Wed, 28 Apr 2010 13:30:34 +0200 haftmann try to observe intended meaning of add_registration interface more closely
Wed, 28 Apr 2010 13:29:39 +0200 haftmann empty class specifcations observe default sort
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;
Fri, 12 Feb 2010 09:49:28 +0100 haftmann tuned comments
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;
Fri, 13 Nov 2009 21:11:15 +0100 wenzelm modernized structure Local_Theory;
Tue, 10 Nov 2009 16:04:57 +0100 wenzelm modernized structure Theory_Target;
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;
Wed, 07 Oct 2009 12:06:04 +0200 haftmann do not use Locale.add_registration_eqs any longer
Thu, 01 Oct 2009 17:11:48 +0200 haftmann proper merge of interpretation equations
Sun, 27 Sep 2009 09:52:25 +0200 haftmann dropped dead code
Sat, 25 Jul 2009 18:44:55 +0200 haftmann improved handling of parameter import; tuned
Mon, 20 Jul 2009 16:49:05 +0200 haftmann dropped add_registration interface in locale
Fri, 10 Jul 2009 07:59:28 +0200 haftmann tuned
Mon, 06 Jul 2009 20:36:38 +0200 wenzelm clarified Thm.of_class/of_sort/class_triv;
Mon, 06 Jul 2009 19:58:52 +0200 wenzelm renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
Thu, 02 Jul 2009 21:26:18 +0200 wenzelm renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
Wed, 24 Jun 2009 21:28:02 +0200 wenzelm renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
Wed, 17 Jun 2009 17:42:36 +0200 haftmann skip_proof where appropriate
Mon, 15 Jun 2009 08:16:09 +0200 haftmann skip_proof not operative here
Sun, 14 Jun 2009 17:20:19 +0200 haftmann using skip_proof where appropriate
Sat, 28 Mar 2009 20:25:23 +0100 wenzelm simplified Locale.activate operations, using generic context;
Sat, 28 Mar 2009 16:00:54 +0100 wenzelm simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;
Thu, 19 Mar 2009 13:28:55 +0100 wenzelm use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
Sat, 07 Mar 2009 22:16:50 +0100 wenzelm more uniform handling of binding in targets and derived elements;
Sat, 07 Mar 2009 11:32:31 +0100 wenzelm Binding.str_of: removed verbose feature, include qualifier in output;
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Tue, 03 Mar 2009 18:32:01 +0100 wenzelm renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
Tue, 03 Mar 2009 14:07:43 +0100 wenzelm Thm.binding;
Fri, 06 Feb 2009 09:05:20 +0100 haftmann more robust failure in error situations
Tue, 03 Feb 2009 21:26:21 +0100 haftmann handling type classes without parameters
Sun, 01 Feb 2009 19:58:02 +0100 haftmann proper declared constants in class expressions
Wed, 28 Jan 2009 16:35:42 +0100 haftmann explicit check for exactly one type variable in class specification elements
Mon, 26 Jan 2009 22:14:19 +0100 haftmann fixed reading of class specs: declare class operations in context
Mon, 26 Jan 2009 08:23:55 +0100 haftmann correct proof of assm_intro rule
Fri, 23 Jan 2009 19:51:49 +0100 haftmann fixed fixme
Wed, 21 Jan 2009 23:40:23 +0100 haftmann no base sort in class import
Wed, 21 Jan 2009 16:47:02 +0100 haftmann improved and corrected reading of class specs -- still draft version
Mon, 19 Jan 2009 08:16:42 +0100 haftmann improved tackling of subclasses
Sun, 18 Jan 2009 10:11:12 +0100 haftmann improved calculation of morphisms and rules
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
Wed, 07 Jan 2009 08:03:25 +0100 haftmann proper local_theory after Class.class
Mon, 05 Jan 2009 15:55:04 +0100 haftmann locale -> old_locale, new_locale -> locale
less more (0) -100 -60 tip