| Sat, 06 Mar 2010 17:53:04 +0100 |
wenzelm |
provide ProofContext.def_type depending on "pattern" mode;
|
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 20:51:51 +0100 |
wenzelm |
clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;
|
file |
diff |
annotate
|
| Thu, 25 Feb 2010 22:06:43 +0100 |
wenzelm |
clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
|
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 17:28:02 +0100 |
berghofe |
Use top-down rewriting to contract abbreviations.
|
file |
diff |
annotate
|
| Tue, 16 Feb 2010 11:59:05 +0100 |
wenzelm |
simplified meaning of ProofContext.verbose;
|
file |
diff |
annotate
|
| Tue, 16 Feb 2010 11:27:29 +0100 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Mon, 15 Feb 2010 17:17:51 +0100 |
wenzelm |
discontinued unnamed infix syntax;
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 22:03:37 +0100 |
wenzelm |
added ML antiquotation @{syntax_const};
|
file |
diff |
annotate
|
| Tue, 02 Feb 2010 11:38:38 +0100 |
blanchet |
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
|
file |
diff |
annotate
|
| Wed, 25 Nov 2009 09:13:46 +0100 |
haftmann |
normalized uncurry take/drop
|
file |
diff |
annotate
|
| Tue, 24 Nov 2009 17:28:25 +0100 |
haftmann |
curried take/drop
|
file |
diff |
annotate
|
| Sun, 15 Nov 2009 19:45:05 +0100 |
wenzelm |
eliminated obsolete thm position tags;
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 22:29:54 +0100 |
wenzelm |
eliminated slightly odd (unused) "axiom" and "assumption" -- collapsed to unspecific "";
|
file |
diff |
annotate
|
| Mon, 09 Nov 2009 20:47:39 +0100 |
wenzelm |
locale_const/target_notation: uniform use of Term.aconv_untyped;
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 20:48:08 +0100 |
wenzelm |
modernized structure Local_Syntax;
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 20:45:23 +0100 |
wenzelm |
modernized structure AutoBind;
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 20:30:40 +0100 |
wenzelm |
modernized structure Context_Position;
|
file |
diff |
annotate
|
| Sun, 01 Nov 2009 15:24:45 +0100 |
wenzelm |
modernized structure Rule_Cases;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 13:24:40 +0100 |
wenzelm |
ProofContext.setmp_verbose_CRITICAL;
|
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 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 19:47:37 +0200 |
wenzelm |
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 21:26:45 +0200 |
wenzelm |
backpatching of structure Proof and ProofContext -- avoid odd aliases;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 15:57:51 +0200 |
wenzelm |
indicate CRITICAL nature of various setmp combinators;
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 22:20:58 +0200 |
wenzelm |
eliminated redundant bindings;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 00:56:19 +0200 |
wenzelm |
moved ProofContext.pretty_thm to Display.pretty_thm etc.;
|
file |
diff |
annotate
|
| Fri, 17 Jul 2009 21:33:00 +0200 |
wenzelm |
tuned/modernized Envir operations;
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 12:10:44 +0200 |
wenzelm |
tuned prepare_patternT: Term.exists_subtype;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2009 13:34:48 +0200 |
wenzelm |
tuned error message;
|
file |
diff |
annotate
|
| Sat, 28 Mar 2009 17:53:33 +0100 |
wenzelm |
renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
|
file |
diff |
annotate
|
| Sat, 28 Mar 2009 17:21:11 +0100 |
wenzelm |
renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
|
file |
diff |
annotate
|
| Sat, 28 Mar 2009 17:08:18 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 28 Mar 2009 16:31:16 +0100 |
wenzelm |
replaced add_binds(_i) by bind_terms -- internal version only;
|
file |
diff |
annotate
|
| Thu, 26 Mar 2009 15:18:50 +0100 |
wenzelm |
pretty_thm_aux etc.: explicit show_status flag;
|
file |
diff |
annotate
|
| Sat, 21 Mar 2009 20:00:23 +0100 |
wenzelm |
removed obsolete pprint operations;
|
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
|
| Wed, 18 Mar 2009 21:55:38 +0100 |
wenzelm |
de-camelized Symbol_Pos;
|
file |
diff |
annotate
|
| Tue, 17 Mar 2009 16:55:21 +0100 |
wenzelm |
reverted abbreviations: improved performance via Item_Net.T;
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 15:54:58 +0100 |
wenzelm |
Assumption.all_prems_of, Assumption.all_assms_of;
|
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
|
| Tue, 10 Mar 2009 22:49:56 +0100 |
wenzelm |
Consts.eq_const is back again (cf. 907da436f8a9) -- required in ProofContext.transfer_syntax to prevent expensive merges of local_consts/global_consts;
|
file |
diff |
annotate
|
| Tue, 10 Mar 2009 21:19:22 +0100 |
wenzelm |
removed obsolete no_base_names;
|
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
|
| Thu, 05 Mar 2009 15:27:07 +0100 |
wenzelm |
eliminated Consts.eq_consts tuning -- this is built into tables and name spaces already;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 11:58:53 +0100 |
wenzelm |
eliminated obsolete ProofContext.full_bname;
|
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
|
| Tue, 03 Mar 2009 14:07:43 +0100 |
wenzelm |
Thm.binding;
|
file |
diff |
annotate
|
| Sun, 01 Mar 2009 23:36:12 +0100 |
wenzelm |
use long names for old-style fold combinators;
|
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, 02 Jan 2009 19:38:13 +0100 |
wenzelm |
added numeral, which supercedes num, xnum, float;
|
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:03 +0100 |
haftmann |
fact table now using name bindings
|
file |
diff |
annotate
|
| Thu, 20 Nov 2008 14:55:25 +0100 |
haftmann |
using name bindings
|
file |
diff |
annotate
|
| Thu, 20 Nov 2008 00:03:47 +0100 |
wenzelm |
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
|
file |
diff |
annotate
|
| Fri, 14 Nov 2008 08:50:10 +0100 |
haftmann |
namify and name_decl combinators
|
file |
diff |
annotate
|
| Mon, 29 Sep 2008 21:45:44 +0200 |
wenzelm |
put_thms: ContextPosition.set_visible false;
|
file |
diff |
annotate
|
| Mon, 29 Sep 2008 21:26:36 +0200 |
wenzelm |
back to plain Position.report for regular references;
|
file |
diff |
annotate
|
| Mon, 29 Sep 2008 14:41:25 +0200 |
wenzelm |
ContextPosition.report;
|
file |
diff |
annotate
|
| Mon, 29 Sep 2008 10:58:04 +0200 |
wenzelm |
added norm_export_morphism;
|
file |
diff |
annotate
|
| Fri, 12 Sep 2008 12:04:20 +0200 |
wenzelm |
added extern_fact (local or global);
|
file |
diff |
annotate
|
| Fri, 12 Sep 2008 10:54:00 +0200 |
wenzelm |
pretty_fact: extern fact name wrt. the given context, assuming that is the proper one for presentation;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 18:01:24 +0200 |
wenzelm |
pretty_fact/results: display base only, since results now come with full names (note that Facts.extern is not really well-defined unless we present the real target context);
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 14:10:32 +0200 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 11:48:54 +0200 |
wenzelm |
type Properties.T;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2008 16:52:52 +0200 |
wenzelm |
retrieve_thms: transfer fact position to result;
|
file |
diff |
annotate
|
| Mon, 11 Aug 2008 18:37:49 +0200 |
wenzelm |
renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);
|
file |
diff |
annotate
|
| Sun, 10 Aug 2008 12:38:25 +0200 |
wenzelm |
read_tyname/const/const_proper: report position;
|
file |
diff |
annotate
|
| Thu, 07 Aug 2008 22:32:01 +0200 |
wenzelm |
parse_token: use Syntax.read_token, pass full position information;
|
file |
diff |
annotate
|
| Wed, 06 Aug 2008 00:12:02 +0200 |
wenzelm |
parse_sort/typ/term/prop: report markup;
|
file |
diff |
annotate
|
| Tue, 05 Aug 2008 13:31:31 +0200 |
wenzelm |
Facts.lookup: return static/dynamic status;
|
file |
diff |
annotate
|
| Sat, 21 Jun 2008 16:18:51 +0200 |
wenzelm |
added query_type/const/class (meta data);
|
file |
diff |
annotate
|
| Thu, 19 Jun 2008 22:05:05 +0200 |
wenzelm |
renamed is_abbrev_mode to abbrev_mode;
|
file |
diff |
annotate
|
| Wed, 18 Jun 2008 22:32:03 +0200 |
wenzelm |
simplified TypeInfer.infer_types;
|
file |
diff |
annotate
|
| Wed, 18 Jun 2008 18:55:07 +0200 |
wenzelm |
export transfer_syntax;
|
file |
diff |
annotate
|
| Fri, 13 Jun 2008 21:04:42 +0200 |
wenzelm |
map_const: soft version, no failure here;
|
file |
diff |
annotate
|
| Thu, 12 Jun 2008 16:41:47 +0200 |
wenzelm |
Facts.dest/export_static: content difference;
|
file |
diff |
annotate
|
| Sun, 18 May 2008 17:03:26 +0200 |
wenzelm |
unparse_term: check PureThy.old_appl_syntax instead of CPure;
|
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:02 +0200 |
wenzelm |
default token translations: observe Sign.is_pretty_global for fixed variables;
|
file |
diff |
annotate
|
| Tue, 22 Apr 2008 08:33:13 +0200 |
haftmann |
exported is_abbrev mode discriminator
|
file |
diff |
annotate
|
| Fri, 18 Apr 2008 23:49:46 +0200 |
wenzelm |
print_cases: proper context for revert_skolem;
|
file |
diff |
annotate
|
| Thu, 17 Apr 2008 22:22:30 +0200 |
wenzelm |
revert_skolem: do not change non-reversible names;
|
file |
diff |
annotate
|
| Thu, 17 Apr 2008 16:30:51 +0200 |
wenzelm |
default token translations with proper markup;
|
file |
diff |
annotate
|
| Wed, 16 Apr 2008 21:53:03 +0200 |
wenzelm |
Facts.extern_static;
|
file |
diff |
annotate
|
| Wed, 16 Apr 2008 17:40:43 +0200 |
wenzelm |
removed obsolete valid_thms;
|
file |
diff |
annotate
|
| Tue, 15 Apr 2008 18:49:28 +0200 |
wenzelm |
Facts.intern, Facts.extern_table;
|
file |
diff |
annotate
|
| Fri, 28 Mar 2008 20:02:04 +0100 |
wenzelm |
Context.>> : operate on Context.generic;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 15:32:15 +0100 |
wenzelm |
eliminated delayed theory setup
|
file |
diff |
annotate
|
| Tue, 25 Mar 2008 19:39:59 +0100 |
wenzelm |
support dynamic facts;
|
file |
diff |
annotate
|
| Thu, 20 Mar 2008 16:04:30 +0100 |
wenzelm |
Facts.Named: include position;
|
file |
diff |
annotate
|
| Thu, 20 Mar 2008 00:20:51 +0100 |
wenzelm |
simplified get_thm(s): back to plain name argument;
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 22:27:57 +0100 |
wenzelm |
renamed datatype thmref to Facts.ref, tuned interfaces;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2008 21:57:36 +0100 |
wenzelm |
valid_thms: get_thms_silent;
|
file |
diff |
annotate
|
| Mon, 17 Mar 2008 20:51:23 +0100 |
wenzelm |
Facts.add_local;
|
file |
diff |
annotate
|
| Sat, 15 Mar 2008 18:08:04 +0100 |
wenzelm |
replaced obsolete FactIndex.T by Facts.T;
|
file |
diff |
annotate
|
| Fri, 14 Mar 2008 08:52:53 +0100 |
haftmann |
added mk_const functions
|
file |
diff |
annotate
|
| Tue, 11 Mar 2008 17:13:04 +0100 |
wenzelm |
put_thms: pass do_props;
|
file |
diff |
annotate
|
| Fri, 07 Mar 2008 13:53:09 +0100 |
haftmann |
dropped local tsigs
|
file |
diff |
annotate
|
| Wed, 05 Mar 2008 21:24:06 +0100 |
wenzelm |
put_thms: do not index facts here (affects prems/this/calculation in particular);
|
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:34 +0100 |
haftmann |
explicit type signature
|
file |
diff |
annotate
|
| Wed, 21 Nov 2007 14:43:50 +0100 |
wenzelm |
intern_skolem: disallow qualified names;
|
file |
diff |
annotate
|
| Sun, 11 Nov 2007 20:29:06 +0100 |
wenzelm |
simplified Consts.dest;
|
file |
diff |
annotate
|
| Thu, 08 Nov 2007 20:08:09 +0100 |
wenzelm |
removed unused read_termTs_schematic, read/cert_vars_legacy, add_fixes_legacy;
|
file |
diff |
annotate
|
| Thu, 08 Nov 2007 14:51:30 +0100 |
wenzelm |
renamed ProofContext.read_const' to ProofContext.read_const_proper;
|
file |
diff |
annotate
|
| Wed, 07 Nov 2007 22:20:11 +0100 |
wenzelm |
export read_const';
|
file |
diff |
annotate
|