src/Pure/Isar/expression.ML
Sat, 31 Jul 2010 21:14:20 +0200 ballarin Make registrations generic data.
Fri, 04 Jun 2010 14:15:56 +0200 wenzelm tuned warning;
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
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;
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;
Mon, 15 Mar 2010 18:59:16 +0100 wenzelm replaced type_syntax/term_syntax by uniform syntax_declaration;
Sun, 07 Mar 2010 12:19:47 +0100 wenzelm modernized structure Object_Logic;
Sun, 07 Mar 2010 11:57:16 +0100 wenzelm modernized structure Local_Defs;
Sun, 21 Feb 2010 22:35:02 +0100 wenzelm slightly more abstract syntax mark/unmark operations;
Fri, 19 Feb 2010 20:41:34 +0100 wenzelm Thm.def_binding;
Thu, 18 Feb 2010 23:38:33 +0100 wenzelm locale: more precise treatment of naming vs. binding;
Tue, 16 Feb 2010 13:26:21 +0100 wenzelm comment;
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;
Fri, 13 Nov 2009 20:41:29 +0100 wenzelm eliminated slightly odd kind argument of LocalTheory.note(s);
Thu, 12 Nov 2009 22:29:54 +0100 wenzelm eliminated slightly odd (unused) "axiom" and "assumption" -- collapsed to unspecific "";
Thu, 12 Nov 2009 22:02:11 +0100 wenzelm eliminated obsolete "internal" kind -- collapsed to unspecific "";
Tue, 10 Nov 2009 16:04:57 +0100 wenzelm modernized structure Theory_Target;
Fri, 30 Oct 2009 13:59:52 +0100 haftmann tuned variable names of bindings; conceal predicate constants
Thu, 29 Oct 2009 16:34:44 +0100 wenzelm eliminated obsolete/unused Thm.kind_internal/is_internal etc.;
Wed, 28 Oct 2009 16:25:27 +0100 wenzelm conceal internal bindings;
Sun, 25 Oct 2009 21:35:46 +0100 wenzelm eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
Wed, 21 Oct 2009 10:15:31 +0200 haftmann removed old-style \ and \\ infixes
Thu, 01 Oct 2009 20:52:18 +0200 ballarin Merged.
Thu, 01 Oct 2009 20:37:33 +0200 ballarin Avoid administrative overhead for identity mixins.
Thu, 01 Oct 2009 11:33:32 +0200 wenzelm merged
Thu, 01 Oct 2009 07:40:25 +0200 ballarin Merged.
Tue, 29 Sep 2009 22:15:54 +0200 ballarin Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
Sat, 19 Sep 2009 18:43:11 +0200 ballarin Explicit management of registration mixins.
Wed, 19 Aug 2009 19:35:46 +0200 ballarin Improved comments and api names.
Wed, 30 Sep 2009 22:24:57 +0200 wenzelm eliminated redundant parameters;
Thu, 03 Sep 2009 15:39:02 +0200 haftmann proper class syntax for sublocale class < expr
Wed, 15 Jul 2009 18:20:08 +0200 haftmann simplification of locale interfaces
Fri, 10 Jul 2009 07:59:44 +0200 haftmann merged
Fri, 10 Jul 2009 07:59:29 +0200 haftmann tuned locale interface
Thu, 09 Jul 2009 22:48:12 +0200 wenzelm renamed structure TermSubst to Term_Subst;
Mon, 30 Mar 2009 15:16:58 +0200 wenzelm prep_full_context_statement: explicit record of flags;
Sun, 29 Mar 2009 19:48:35 +0200 wenzelm merged
Sun, 29 Mar 2009 17:38:01 +0200 ballarin Merged.
Sun, 29 Mar 2009 17:22:17 +0200 ballarin Normalise equation only for morphism, not thm stored in theory.
Sun, 29 Mar 2009 19:41:04 +0200 wenzelm tuned;
Sun, 29 Mar 2009 18:06:14 +0200 wenzelm simplified Element.activate(_i): singleton version;
Sun, 29 Mar 2009 17:47:58 +0200 wenzelm tuned;
Sun, 29 Mar 2009 16:13:44 +0200 wenzelm unified binding prefix terminology;
Sat, 28 Mar 2009 20:25:23 +0100 wenzelm simplified Locale.activate operations, using generic context;
Sat, 28 Mar 2009 17:53:33 +0100 wenzelm renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
Sat, 28 Mar 2009 17:21:49 +0100 wenzelm define_prefs: removed redundant Drule.gen_all, which is already part of the norm_hhf stage of Assumption.assume;
Sat, 28 Mar 2009 16:00:54 +0100 wenzelm simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;
Thu, 26 Mar 2009 17:00:59 +0100 wenzelm register_locale: produce stamps at the spot where elements are registered;
Thu, 19 Mar 2009 13:28:55 +0100 wenzelm use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
Thu, 12 Mar 2009 13:18:42 +0100 wenzelm renamed sticky_prefix to mandatory_path;
Thu, 12 Mar 2009 12:04:27 +0100 wenzelm replaced old-style add_path/no_base_names by sticky_prefix;
Wed, 11 Mar 2009 15:38:25 +0100 wenzelm Thm.def_binding_optional;
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 15:12:52 +0100 wenzelm Binding.str_of;
less more (0) -100 -60 tip