src/Pure/sign.ML
Thu, 18 Feb 2010 20:46:46 +0100 wenzelm more systematic treatment of qualified names derived from binding;
Mon, 15 Feb 2010 17:17:51 +0100 wenzelm discontinued unnamed infix syntax;
Mon, 04 Jan 2010 23:20:35 +0100 wenzelm discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
Mon, 04 Jan 2010 14:09:56 +0100 haftmann dropped copy operation for legacy TheoryDataFun
Tue, 17 Nov 2009 14:50:55 +0100 wenzelm uniform new_group/reset_group;
Mon, 02 Nov 2009 20:38:46 +0100 wenzelm modernized structure Primitive_Defs;
Sun, 25 Oct 2009 21:35:46 +0100 wenzelm eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
Sun, 25 Oct 2009 20:54:21 +0100 wenzelm maintain theory name via name space, not tags;
Sun, 25 Oct 2009 19:17:42 +0100 wenzelm more direct access to naming;
Sun, 25 Oct 2009 12:27:21 +0100 wenzelm allow name space entries to be "concealed" -- via binding/naming/local_theory;
Sat, 24 Oct 2009 21:30:33 +0200 wenzelm maintain position of formal entities via name space;
Sat, 24 Oct 2009 19:47:37 +0200 wenzelm renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
Wed, 30 Sep 2009 22:27:20 +0200 wenzelm removed redundant Sign.certify_prop, use Sign.cert_prop instead;
Mon, 06 Jul 2009 22:41:00 +0200 wenzelm witness_sorts: proper type witnesses for hyps, not invented "'hyp" variables;
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, 14 Mar 2009 00:13:50 +0100 wenzelm removed obsolete no_base_names naming policy;
Thu, 12 Mar 2009 13:18:42 +0100 wenzelm renamed sticky_prefix to mandatory_path;
Wed, 11 Mar 2009 16:36:27 +0100 wenzelm eliminated qualified_names naming policy: qualified names are only permitted via explicit Binding.qualify/qualified_name etc. (NB: user-level outer syntax should never do this);
Wed, 11 Mar 2009 15:44:12 +0100 wenzelm removed obsolete absolute_path -- use root_path with qualified binding;
Tue, 10 Mar 2009 21:20:01 +0100 wenzelm explicit root_path, parent_path;
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:12:07 +0100 wenzelm replace old bstring by binding for logical primitives: class, type, const etc.;
Thu, 05 Mar 2009 12:08:00 +0100 wenzelm renamed NameSpace.base to NameSpace.base_name;
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:09:08 +0100 wenzelm Binding.str_of;
Fri, 27 Feb 2009 16:38:52 +0100 wenzelm eliminated NJ's List.nth;
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids;
Wed, 21 Jan 2009 16:47:32 +0100 haftmann binding is alias for Binding.T
Fri, 05 Dec 2008 18:43:42 +0100 haftmann Name.name_of -> Binding.base_name
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code
Mon, 01 Dec 2008 19:41:16 +0100 haftmann new Binding module
Thu, 20 Nov 2008 19:06:02 +0100 haftmann dropped legacy naming code
Thu, 20 Nov 2008 14:55:25 +0100 haftmann using name bindings
Fri, 14 Nov 2008 08:50:10 +0100 haftmann namify and name_decl combinators
Wed, 03 Sep 2008 17:47:34 +0200 wenzelm declare_const: Name.binding, store/report position;
Wed, 27 Aug 2008 11:48:54 +0200 wenzelm type Properties.T;
Fri, 20 Jun 2008 21:00:26 +0200 haftmann type constructors now with markup
Thu, 19 Jun 2008 22:05:01 +0200 wenzelm moved get_sort to Isar/proof_context.ML;
Wed, 18 Jun 2008 18:55:05 +0200 wenzelm removed obsolete term reading operations (cf. old_goals.ML for legacy emulations);
Sat, 14 Jun 2008 17:26:14 +0200 wenzelm certify_term: reject qualified frees;
Fri, 13 Jun 2008 21:04:42 +0200 wenzelm map_const: soft version, no failure here;
Fri, 23 May 2008 21:20:26 +0200 wenzelm add constants: set Markup.theory_nameN in tags;
Sun, 18 May 2008 15:04:09 +0200 wenzelm moved global pretty/string_of functions from Sign to Syntax;
Sat, 17 May 2008 14:27:01 +0200 wenzelm added pretty_global flag;
Thu, 17 Apr 2008 16:30:47 +0200 wenzelm token translations: context dependent, result Pretty.T;
Tue, 15 Apr 2008 18:49:22 +0200 wenzelm removed obsolete SIGN_THEORY -- no name aliases in structure Theory;
Sun, 13 Apr 2008 16:40:02 +0200 wenzelm tsig: removed unnecessary universal witness;
Sat, 12 Apr 2008 17:00:45 +0200 wenzelm rep_cterm/rep_thm: no longer dereference theory_ref;
Fri, 14 Mar 2008 08:52:53 +0100 haftmann added mk_const functions
Tue, 27 Nov 2007 16:48:38 +0100 wenzelm standard_parse_term: check ambiguous results without changing the result yet;
Fri, 23 Nov 2007 21:09:30 +0100 haftmann separated typedecl module, providing typedecl command with interpretation
Sun, 11 Nov 2007 14:00:09 +0100 wenzelm syntax operations: turned extend'' into update'' (absorb duplicates);
Sat, 10 Nov 2007 23:03:56 +0100 wenzelm notation: based on Syntax.update_const_gram (avoids duplicates);
Fri, 09 Nov 2007 19:37:35 +0100 wenzelm tyabbr/syntax/consts: replaced obsolete read_typ by Syntax.parse_typ/certify_typ;
Thu, 08 Nov 2007 20:08:02 +0100 wenzelm removed unused read_def_terms';
Wed, 07 Nov 2007 16:42:55 +0100 wenzelm removed obsolete Sign.read_tyname/const (cf. ProofContext);
Sat, 20 Oct 2007 18:54:30 +0200 wenzelm no_variables: tuned error msg;
Wed, 17 Oct 2007 23:16:30 +0200 wenzelm removed unused set_policy;
less more (0) -300 -100 -60 tip