src/Pure/Isar/typedecl.ML
Sun, 18 Mar 2012 13:04:22 +0100 wenzelm maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
Sun, 17 Apr 2011 21:42:47 +0200 wenzelm added Binding.print convenience, which includes quote already;
Sun, 17 Apr 2011 19:54:04 +0200 wenzelm report Name_Space.declare/define, relatively to context;
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context;
Fri, 27 Aug 2010 19:43:28 +0200 wenzelm more careful treatment of context visibility flag wrt. spurious warnings;
Thu, 26 Aug 2010 15:48:08 +0200 wenzelm renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
Thu, 12 Aug 2010 13:23:46 +0200 haftmann Named_Target.theory_init
Wed, 11 Aug 2010 14:45:38 +0200 haftmann renamed Theory_Target to the more appropriate Named_Target
Wed, 28 Apr 2010 16:11:13 +0200 wenzelm tuned user-level type abbrevs: explicit warning concerning ignored sort constraints -- sorts never affect formation of types and type abbrevs strip sorts internally;
Fri, 16 Apr 2010 22:45:07 +0200 wenzelm replaced old Sign.add_tyabbrs(_i) by Sign.add_type_abbrev (without mixfix);
Fri, 16 Apr 2010 20:56:40 +0200 wenzelm allow syntax types within abbreviations;
Fri, 16 Apr 2010 19:43:06 +0200 wenzelm local type abbreviations;
Thu, 15 Apr 2010 20:31:21 +0200 wenzelm explicit ProofContext.check_tfree;
Thu, 15 Apr 2010 18:09:22 +0200 wenzelm replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo;
Fri, 19 Mar 2010 00:41:34 +0100 wenzelm support type arguments with sort constraints;
Thu, 18 Mar 2010 22:56:32 +0100 wenzelm eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
Sat, 13 Mar 2010 14:41:37 +0100 wenzelm added typedecl_wrt, which affects default sorts of type args;
Thu, 11 Mar 2010 18:52:50 +0100 wenzelm actually apply morphism to binding;
Tue, 09 Mar 2010 23:32:13 +0100 wenzelm localized typedecl;
Sun, 07 Mar 2010 12:47:02 +0100 wenzelm separate structure Typedecl;
less more (0) tip