Sun, 05 Sep 2010 19:47:40 +0200 |
wenzelm |
pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Wed, 28 Apr 2010 11:13:11 +0200 |
wenzelm |
more systematic naming of tsig operations;
|
file |
diff |
annotate
|
Wed, 28 Apr 2010 11:09:19 +0200 |
wenzelm |
modernized/simplified Sign.set_defsort;
|
file |
diff |
annotate
|
Fri, 16 Apr 2010 22:45:07 +0200 |
wenzelm |
replaced old Sign.add_tyabbrs(_i) by Sign.add_type_abbrev (without mixfix);
|
file |
diff |
annotate
|
Thu, 15 Apr 2010 20:37:27 +0200 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
Sat, 27 Mar 2010 17:36:32 +0100 |
wenzelm |
disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Mon, 15 Mar 2010 21:59:28 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Mon, 15 Mar 2010 21:57:35 +0100 |
wenzelm |
moved old Sign.intern_term to the place where it is still used;
|
file |
diff |
annotate
|
Tue, 09 Mar 2010 23:29:04 +0100 |
wenzelm |
aliases for class/type/const;
|
file |
diff |
annotate
|
Tue, 09 Mar 2010 14:35:02 +0100 |
wenzelm |
added ProofContext.tsig_of -- proforma version for local name space only, not logical content;
|
file |
diff |
annotate
|
Wed, 03 Mar 2010 00:28:22 +0100 |
wenzelm |
authentic syntax for classes and type constructors;
|
file |
diff |
annotate
|
Mon, 01 Mar 2010 17:07:36 +0100 |
wenzelm |
more uniform treatment of syntax for types vs. consts;
|
file |
diff |
annotate
|
Sat, 27 Feb 2010 13:32:18 +0100 |
wenzelm |
read_class: perform actual read, with source position;
|
file |
diff |
annotate
|
Thu, 25 Feb 2010 22:05:34 +0100 |
wenzelm |
provide direct access to the different kinds of type declarations;
|
file |
diff |
annotate
|
Sun, 21 Feb 2010 22:35:02 +0100 |
wenzelm |
slightly more abstract syntax mark/unmark operations;
|
file |
diff |
annotate
|
Sun, 21 Feb 2010 21:08:25 +0100 |
wenzelm |
authentic syntax for *all* term constants;
|
file |
diff |
annotate
|
Thu, 18 Feb 2010 20:46:46 +0100 |
wenzelm |
more systematic treatment of qualified names derived from binding;
|
file |
diff |
annotate
|
Mon, 15 Feb 2010 17:17:51 +0100 |
wenzelm |
discontinued unnamed infix syntax;
|
file |
diff |
annotate
|
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);
|
file |
diff |
annotate
|
Mon, 04 Jan 2010 14:09:56 +0100 |
haftmann |
dropped copy operation for legacy TheoryDataFun
|
file |
diff |
annotate
|
Tue, 17 Nov 2009 14:50:55 +0100 |
wenzelm |
uniform new_group/reset_group;
|
file |
diff |
annotate
|
Mon, 02 Nov 2009 20:38:46 +0100 |
wenzelm |
modernized structure Primitive_Defs;
|
file |
diff |
annotate
|
Sun, 25 Oct 2009 21:35:46 +0100 |
wenzelm |
eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
|
file |
diff |
annotate
|
Sun, 25 Oct 2009 20:54:21 +0100 |
wenzelm |
maintain theory name via name space, not tags;
|
file |
diff |
annotate
|
Sun, 25 Oct 2009 19:17:42 +0100 |
wenzelm |
more direct access to naming;
|
file |
diff |
annotate
|
Sun, 25 Oct 2009 12:27:21 +0100 |
wenzelm |
allow name space entries to be "concealed" -- via binding/naming/local_theory;
|
file |
diff |
annotate
|
Sat, 24 Oct 2009 21:30:33 +0200 |
wenzelm |
maintain position of formal entities via name space;
|
file |
diff |
annotate
|
Sat, 24 Oct 2009 19:47:37 +0200 |
wenzelm |
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
|
file |
diff |
annotate
|
Wed, 30 Sep 2009 22:27:20 +0200 |
wenzelm |
removed redundant Sign.certify_prop, use Sign.cert_prop instead;
|
file |
diff |
annotate
|
Mon, 06 Jul 2009 22:41:00 +0200 |
wenzelm |
witness_sorts: proper type witnesses for hyps, not invented "'hyp" variables;
|
file |
diff |
annotate
|
Thu, 19 Mar 2009 13:28:55 +0100 |
wenzelm |
use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
|
file |
diff |
annotate
|
Sat, 14 Mar 2009 00:13:50 +0100 |
wenzelm |
removed obsolete no_base_names naming policy;
|
file |
diff |
annotate
|
Thu, 12 Mar 2009 13:18:42 +0100 |
wenzelm |
renamed sticky_prefix to mandatory_path;
|
file |
diff |
annotate
|
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);
|
file |
diff |
annotate
|
Wed, 11 Mar 2009 15:44:12 +0100 |
wenzelm |
removed obsolete absolute_path -- use root_path with qualified binding;
|
file |
diff |
annotate
|
Tue, 10 Mar 2009 21:20:01 +0100 |
wenzelm |
explicit root_path, parent_path;
|
file |
diff |
annotate
|
Sun, 08 Mar 2009 17:26:14 +0100 |
wenzelm |
moved basic algebra of long names from structure NameSpace to Long_Name;
|
file |
diff |
annotate
|
Sat, 07 Mar 2009 22:12:07 +0100 |
wenzelm |
replace old bstring by binding for logical primitives: class, type, const etc.;
|
file |
diff |
annotate
|
Thu, 05 Mar 2009 12:08:00 +0100 |
wenzelm |
renamed NameSpace.base to NameSpace.base_name;
|
file |
diff |
annotate
|
Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Tue, 03 Mar 2009 15:09:08 +0100 |
wenzelm |
Binding.str_of;
|
file |
diff |
annotate
|
Fri, 27 Feb 2009 16:38:52 +0100 |
wenzelm |
eliminated NJ's List.nth;
|
file |
diff |
annotate
|
Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
Wed, 21 Jan 2009 16:47:32 +0100 |
haftmann |
binding is alias for Binding.T
|
file |
diff |
annotate
|
Fri, 05 Dec 2008 18:43:42 +0100 |
haftmann |
Name.name_of -> Binding.base_name
|
file |
diff |
annotate
|
Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
Mon, 01 Dec 2008 19:41:16 +0100 |
haftmann |
new Binding module
|
file |
diff |
annotate
|
Thu, 20 Nov 2008 19:06:02 +0100 |
haftmann |
dropped legacy naming code
|
file |
diff |
annotate
|
Thu, 20 Nov 2008 14:55:25 +0100 |
haftmann |
using name bindings
|
file |
diff |
annotate
|
Fri, 14 Nov 2008 08:50:10 +0100 |
haftmann |
namify and name_decl combinators
|
file |
diff |
annotate
|
Wed, 03 Sep 2008 17:47:34 +0200 |
wenzelm |
declare_const: Name.binding, store/report position;
|
file |
diff |
annotate
|
Wed, 27 Aug 2008 11:48:54 +0200 |
wenzelm |
type Properties.T;
|
file |
diff |
annotate
|
Fri, 20 Jun 2008 21:00:26 +0200 |
haftmann |
type constructors now with markup
|
file |
diff |
annotate
|
Thu, 19 Jun 2008 22:05:01 +0200 |
wenzelm |
moved get_sort to Isar/proof_context.ML;
|
file |
diff |
annotate
|
Wed, 18 Jun 2008 18:55:05 +0200 |
wenzelm |
removed obsolete term reading operations (cf. old_goals.ML for legacy emulations);
|
file |
diff |
annotate
|
Sat, 14 Jun 2008 17:26:14 +0200 |
wenzelm |
certify_term: reject qualified frees;
|
file |
diff |
annotate
|
Fri, 13 Jun 2008 21:04:42 +0200 |
wenzelm |
map_const: soft version, no failure here;
|
file |
diff |
annotate
|
Fri, 23 May 2008 21:20:26 +0200 |
wenzelm |
add constants: set Markup.theory_nameN in tags;
|
file |
diff |
annotate
|
Sun, 18 May 2008 15:04:09 +0200 |
wenzelm |
moved global pretty/string_of functions from Sign to Syntax;
|
file |
diff |
annotate
|
Sat, 17 May 2008 14:27:01 +0200 |
wenzelm |
added pretty_global flag;
|
file |
diff |
annotate
|
Thu, 17 Apr 2008 16:30:47 +0200 |
wenzelm |
token translations: context dependent, result Pretty.T;
|
file |
diff |
annotate
|
Tue, 15 Apr 2008 18:49:22 +0200 |
wenzelm |
removed obsolete SIGN_THEORY -- no name aliases in structure Theory;
|
file |
diff |
annotate
|
Sun, 13 Apr 2008 16:40:02 +0200 |
wenzelm |
tsig: removed unnecessary universal witness;
|
file |
diff |
annotate
|
Sat, 12 Apr 2008 17:00:45 +0200 |
wenzelm |
rep_cterm/rep_thm: no longer dereference theory_ref;
|
file |
diff |
annotate
|
Fri, 14 Mar 2008 08:52:53 +0100 |
haftmann |
added mk_const functions
|
file |
diff |
annotate
|
Tue, 27 Nov 2007 16:48:38 +0100 |
wenzelm |
standard_parse_term: check ambiguous results without changing the result yet;
|
file |
diff |
annotate
|
Fri, 23 Nov 2007 21:09:30 +0100 |
haftmann |
separated typedecl module, providing typedecl command with interpretation
|
file |
diff |
annotate
|
Sun, 11 Nov 2007 14:00:09 +0100 |
wenzelm |
syntax operations: turned extend'' into update'' (absorb duplicates);
|
file |
diff |
annotate
|
Sat, 10 Nov 2007 23:03:56 +0100 |
wenzelm |
notation: based on Syntax.update_const_gram (avoids duplicates);
|
file |
diff |
annotate
|
Fri, 09 Nov 2007 19:37:35 +0100 |
wenzelm |
tyabbr/syntax/consts: replaced obsolete read_typ by Syntax.parse_typ/certify_typ;
|
file |
diff |
annotate
|
Thu, 08 Nov 2007 20:08:02 +0100 |
wenzelm |
removed unused read_def_terms';
|
file |
diff |
annotate
|
Wed, 07 Nov 2007 16:42:55 +0100 |
wenzelm |
removed obsolete Sign.read_tyname/const (cf. ProofContext);
|
file |
diff |
annotate
|
Sat, 20 Oct 2007 18:54:30 +0200 |
wenzelm |
no_variables: tuned error msg;
|
file |
diff |
annotate
|
Wed, 17 Oct 2007 23:16:30 +0200 |
wenzelm |
removed unused set_policy;
|
file |
diff |
annotate
|
Tue, 16 Oct 2007 17:06:11 +0200 |
wenzelm |
add_abbrev: removed Logic.legacy_varifyT, do not unvarify result (again);
|
file |
diff |
annotate
|
Mon, 15 Oct 2007 21:08:36 +0200 |
wenzelm |
renamed Consts.the_declaration to Consts.the_type;
|
file |
diff |
annotate
|
Sat, 13 Oct 2007 17:16:42 +0200 |
wenzelm |
add_abbrevs: unvarify result;
|
file |
diff |
annotate
|
Thu, 11 Oct 2007 19:10:23 +0200 |
wenzelm |
dest/cert_def: replaced Pretty.pp by explicit Proof.context;
|
file |
diff |
annotate
|
Thu, 11 Oct 2007 16:38:57 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Thu, 11 Oct 2007 16:05:23 +0200 |
wenzelm |
replaced Sign.add_consts_authentic by Sign.declare_const;
|
file |
diff |
annotate
|
Wed, 10 Oct 2007 17:31:56 +0200 |
wenzelm |
generalized notation interface (add or del);
|
file |
diff |
annotate
|
Tue, 09 Oct 2007 00:20:21 +0200 |
wenzelm |
generic Syntax.pretty/string_of operations;
|
file |
diff |
annotate
|
Sun, 30 Sep 2007 16:20:38 +0200 |
wenzelm |
add_consts_authentic/add_abbrev: tags (Markup.property list);
|
file |
diff |
annotate
|
Sat, 29 Sep 2007 21:39:46 +0200 |
wenzelm |
removed obsolete external interface add_const_constraint;
|
file |
diff |
annotate
|
Wed, 26 Sep 2007 20:50:34 +0200 |
wenzelm |
added minimize_sort, complete_sort;
|
file |
diff |
annotate
|
Tue, 25 Sep 2007 13:28:37 +0200 |
wenzelm |
Syntax.parse/check/read;
|
file |
diff |
annotate
|
Sat, 22 Sep 2007 17:45:56 +0200 |
wenzelm |
certify': proper do_expand argument (which observes force_expand consts) instead of home-grown normalize;
|
file |
diff |
annotate
|
Sat, 01 Sep 2007 18:17:42 +0200 |
wenzelm |
read_def_terms: replaced full Syntax.check_typs by certify_typ, to workaround problems with illegal schematic type vars;
|
file |
diff |
annotate
|
Thu, 30 Aug 2007 15:04:44 +0200 |
wenzelm |
infer_types: general check_typs instead of Type.cert_typ_mode;
|
file |
diff |
annotate
|
Mon, 20 Aug 2007 23:41:37 +0200 |
wenzelm |
read_def_terms: moved disambig to syntax.ML;
|
file |
diff |
annotate
|
Tue, 14 Aug 2007 23:22:55 +0200 |
wenzelm |
replaced certify_typ_syntax/abbrev by certify_typ_mode;
|
file |
diff |
annotate
|
Tue, 14 Aug 2007 13:20:18 +0200 |
wenzelm |
PrimitiveDefs.dest_def;
|
file |
diff |
annotate
|
Sun, 12 Aug 2007 18:53:05 +0200 |
wenzelm |
read_def_terms': restrict scope of disambiguation to individual term;
|
file |
diff |
annotate
|
Fri, 03 Aug 2007 16:28:21 +0200 |
wenzelm |
certify: no check_thy here;
|
file |
diff |
annotate
|
Tue, 24 Jul 2007 19:44:35 +0200 |
wenzelm |
moved exception capture/release to structure Exn;
|
file |
diff |
annotate
|
Mon, 09 Jul 2007 11:44:20 +0200 |
wenzelm |
type output = string indicates raw system output;
|
file |
diff |
annotate
|
Sat, 07 Jul 2007 00:14:56 +0200 |
wenzelm |
simplified pretty token metric: type int;
|
file |
diff |
annotate
|
Mon, 07 May 2007 00:49:59 +0200 |
wenzelm |
simplified DataFun interfaces;
|
file |
diff |
annotate
|
Thu, 26 Apr 2007 14:24:14 +0200 |
wenzelm |
renamed some old names Theory.xxx to Sign.xxx;
|
file |
diff |
annotate
|
Thu, 26 Apr 2007 12:00:05 +0200 |
wenzelm |
renamed some old names Theory.xxx to Sign.xxx;
|
file |
diff |
annotate
|
Sat, 21 Apr 2007 11:07:45 +0200 |
wenzelm |
export get_sort (belongs to Syntax module);
|
file |
diff |
annotate
|
Sun, 15 Apr 2007 23:25:50 +0200 |
wenzelm |
removed obsolete TypeInfer.logicT -- use dummyT;
|
file |
diff |
annotate
|
Sun, 15 Apr 2007 14:31:54 +0200 |
wenzelm |
removed obsolete infer_types(_simult);
|
file |
diff |
annotate
|
Sat, 14 Apr 2007 17:36:14 +0200 |
wenzelm |
read_typ_XXX: no sorts;
|
file |
diff |
annotate
|
Fri, 19 Jan 2007 22:08:20 +0100 |
wenzelm |
moved ML translation interfaces to isar_cmd.ML;
|
file |
diff |
annotate
|
Fri, 19 Jan 2007 13:09:33 +0100 |
wenzelm |
adapted ML context operations;
|
file |
diff |
annotate
|
Fri, 29 Dec 2006 17:24:43 +0100 |
wenzelm |
replaced classes by all_classes (topologically sorted);
|
file |
diff |
annotate
|
Tue, 12 Dec 2006 20:49:23 +0100 |
wenzelm |
add_abbrev: tuned signature;
|
file |
diff |
annotate
|
Mon, 11 Dec 2006 21:39:26 +0100 |
wenzelm |
advanced translation functions: Proof.context;
|
file |
diff |
annotate
|
Sun, 10 Dec 2006 15:30:39 +0100 |
wenzelm |
added no_frees;
|
file |
diff |
annotate
|
Sat, 09 Dec 2006 18:05:41 +0100 |
wenzelm |
tuned Consts signature;
|
file |
diff |
annotate
|
Thu, 07 Dec 2006 21:08:48 +0100 |
wenzelm |
simplified add_abbrev -- single argument;
|
file |
diff |
annotate
|
Thu, 07 Dec 2006 17:58:46 +0100 |
wenzelm |
simplified add_abbrevs: no mixfix;
|
file |
diff |
annotate
|
Wed, 06 Dec 2006 21:18:58 +0100 |
wenzelm |
add_abbrevs: moved common parts to consts.ML;
|
file |
diff |
annotate
|
Tue, 05 Dec 2006 22:14:46 +0100 |
wenzelm |
add_notation: permissive about undeclared consts;
|
file |
diff |
annotate
|