src/Pure/Isar/locale.ML
Fri, 14 Nov 2008 14:00:52 +0100 ballarin Made local_note_prefix public.
Fri, 14 Nov 2008 08:50:10 +0100 haftmann namify and name_decl combinators
Thu, 13 Nov 2008 14:19:10 +0100 haftmann proper name morphisms for locales
Mon, 10 Nov 2008 19:42:22 +0100 haftmann restruced naming code in anticipation of introduction of name morphisms
Mon, 10 Nov 2008 08:18:58 +0100 haftmann using explicit interpretaton prefix in Name.binding (still on the surface)
Thu, 30 Oct 2008 10:57:45 +0100 ballarin Dropped context element 'includes'.
Mon, 27 Oct 2008 16:14:51 +0100 ballarin Extension of interface: declarations_of.
Fri, 26 Sep 2008 19:07:56 +0200 wenzelm eliminated polymorphic equality;
Wed, 17 Sep 2008 15:21:30 +0200 ballarin Public interface to interpretation morphism.
Tue, 16 Sep 2008 12:27:05 +0200 ballarin Clearer separation of interpretation frontend and backend.
Wed, 03 Sep 2008 17:47:30 +0200 wenzelm Sign.declare_const: Name.binding;
Wed, 03 Sep 2008 11:44:48 +0200 wenzelm Name.qualified;
Tue, 02 Sep 2008 17:31:20 +0200 ballarin Interpretation commands no longer accept interpretation attributes.
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;
Thu, 28 Aug 2008 22:08:11 +0200 haftmann no parameter prefix for class interpretation
Wed, 27 Aug 2008 17:54:31 +0200 ballarin Consistent naming of theorems in interpretation.
Wed, 27 Aug 2008 12:00:28 +0200 wenzelm get rid of tabs;
Tue, 26 Aug 2008 16:04:22 +0200 ballarin Reorganisation of registration code.
Thu, 14 Aug 2008 16:52:46 +0200 wenzelm moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
Wed, 06 Aug 2008 16:41:40 +0200 ballarin Interpretation command (theory/proof context) no longer simplifies goal.
Fri, 01 Aug 2008 17:41:37 +0200 ballarin Removed import and lparams from locale record.
Wed, 30 Jul 2008 07:33:59 +0200 haftmann facts_of
Tue, 29 Jul 2008 08:15:44 +0200 haftmann tuned; explicit export of element accessors
Sat, 26 Jul 2008 09:00:26 +0200 haftmann tuned function name
Fri, 25 Jul 2008 12:03:32 +0200 haftmann dropped locale (open)
Sun, 18 May 2008 15:04:41 +0200 wenzelm Syntax.string_of_typ: proper context;
Mon, 14 Apr 2008 17:54:56 +0200 ballarin Changed naming scheme for theorems generated by interpretations.
Sat, 12 Apr 2008 17:00:48 +0200 wenzelm replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
Fri, 28 Mar 2008 20:02:04 +0100 wenzelm Context.>> : operate on Context.generic;
Thu, 27 Mar 2008 15:32:15 +0100 wenzelm eliminated delayed theory setup
Thu, 20 Mar 2008 00:20:49 +0100 wenzelm renamed former get_thms(_silent) to get_fact(_silent);
Mon, 17 Mar 2008 18:36:04 +0100 wenzelm closeup: recover original order of free variables!
Wed, 05 Mar 2008 22:58:11 +0100 wenzelm closeup: minor tuning of term traversal;
Mon, 17 Dec 2007 17:57:52 +0100 haftmann explicit closing of derived witnesses
Thu, 13 Dec 2007 07:09:07 +0100 haftmann memorizing and exporting destruction rules
Thu, 08 Nov 2007 22:19:43 +0100 wenzelm avoid "import" as identifier, which is a keyword in Alice;
Mon, 05 Nov 2007 17:48:51 +0100 ballarin Use of export rather than standard in interpretation.
Fri, 02 Nov 2007 18:53:01 +0100 haftmann generic tactic Method.intros_tac
Fri, 19 Oct 2007 12:22:12 +0200 ballarin Interpretation equations may have name and/or attribute;
Wed, 17 Oct 2007 23:16:34 +0200 wenzelm locale pred: authentic syntax, tuned aprop_tr' accordingly;
Wed, 17 Oct 2007 13:55:37 +0200 wenzelm clarified naming conventions of 'parse' and 'check' (as opposed to former 'cert');
Mon, 15 Oct 2007 15:29:43 +0200 haftmann canonical interpretation interface
Fri, 12 Oct 2007 14:42:30 +0200 haftmann tuned
Wed, 10 Oct 2007 17:32:00 +0200 wenzelm removed redundant strip_vars/abs_eqn, use improved Drule.abs_def instead;
Wed, 10 Oct 2007 10:55:37 +0200 ballarin Prepare proper interface of interpretation_i, interpret_i.
Tue, 09 Oct 2007 00:20:13 +0200 wenzelm generic Syntax.pretty/string_of operations;
Mon, 01 Oct 2007 12:24:07 +0200 ballarin Theory/context data restructured; simplified interface for printing of interpretations.
Sat, 29 Sep 2007 08:58:56 +0200 haftmann exported intern_expr
Mon, 24 Sep 2007 21:07:38 +0200 wenzelm eliminated ProofContext.read_termTs;
Tue, 18 Sep 2007 18:50:17 +0200 ballarin Morphisms applied in global interpretations behave correctly on types and terms.
Tue, 04 Sep 2007 14:32:29 +0200 ballarin Improved comment.
Sat, 28 Jul 2007 20:40:24 +0200 wenzelm tuned signature;
Fri, 27 Jul 2007 20:11:49 +0200 wenzelm Druke.dummy_thm;
Mon, 23 Jul 2007 13:47:48 +0200 ballarin interpretation: unfolding of equations;
Sun, 08 Jul 2007 19:51:58 +0200 wenzelm replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
Thu, 05 Jul 2007 20:01:28 +0200 wenzelm simplified ObjectLogic.atomize;
Tue, 19 Jun 2007 23:15:27 +0200 wenzelm balanced conjunctions;
Sun, 03 Jun 2007 23:16:56 +0200 wenzelm added gen_merge_lists/merge_lists/merge_alists (legacy operations from library.ML);
Thu, 31 May 2007 23:47:36 +0200 wenzelm simplified/unified list fold;
less more (0) -100 -60 tip