| 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
|
| Wed, 07 Nov 2007 16:43:00 +0100 |
wenzelm |
discontinued ProofContext.read_prop_legacy;
|
file |
diff |
annotate
|
| Tue, 06 Nov 2007 22:50:37 +0100 |
wenzelm |
read_const/legacy_intern_skolem: cover consts within the local scope;
|
file |
diff |
annotate
|
| Wed, 24 Oct 2007 17:17:43 +0200 |
wenzelm |
parse_term: invoke full Syntax.check_term, not just standard_infer_types;
|
file |
diff |
annotate
|
| Tue, 23 Oct 2007 13:29:17 +0200 |
wenzelm |
added XCONST syntax (keeps original spelling of const);
|
file |
diff |
annotate
|
| Sun, 21 Oct 2007 14:21:54 +0200 |
wenzelm |
context_const_ast_tr: proper const_syntax_name (cf. @{const_syntax});
|
file |
diff |
annotate
|
| Fri, 19 Oct 2007 16:13:53 +0200 |
wenzelm |
do not export standard_infer_types;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2007 23:12:57 +0200 |
haftmann |
exported standard_term_check
|
file |
diff |
annotate
|
| Tue, 16 Oct 2007 19:45:57 +0200 |
wenzelm |
Syntax.(un)check: explicit result option;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2007 17:06:18 +0200 |
wenzelm |
added revert_abbrev;
|
file |
diff |
annotate
|
| Mon, 15 Oct 2007 15:29:45 +0200 |
haftmann |
swapped constant components
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 19:10:24 +0200 |
wenzelm |
replaced Term.equiv_types by Type.similar_types;
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 16:05:30 +0200 |
wenzelm |
moved ProofContext.pp to Syntax.pp;
|
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:22 +0200 |
wenzelm |
generic Syntax.pretty/string_of operations;
|
file |
diff |
annotate
|
| Tue, 02 Oct 2007 16:06:41 +0200 |
wenzelm |
export tsig_of;
|
file |
diff |
annotate
|
| Sun, 30 Sep 2007 16:20:40 +0200 |
wenzelm |
add_abbrev: tags (Markup.property list);
|
file |
diff |
annotate
|
| Sun, 30 Sep 2007 11:55:14 +0200 |
wenzelm |
standard_term_check: include expand_abbrevs (back again);
|
file |
diff |
annotate
|
| Sat, 29 Sep 2007 21:39:52 +0200 |
wenzelm |
removed redundant const_constraint;
|
file |
diff |
annotate
|
| Sat, 29 Sep 2007 08:58:57 +0200 |
haftmann |
exported constraint interfaces
|
file |
diff |
annotate
|
| Mon, 24 Sep 2007 21:07:38 +0200 |
wenzelm |
eliminated ProofContext.read_termTs;
|
file |
diff |
annotate
|
| Sun, 23 Sep 2007 23:39:42 +0200 |
wenzelm |
removed dead code;
|
file |
diff |
annotate
|
| Sun, 23 Sep 2007 23:00:01 +0200 |
wenzelm |
made smlnj happy;
|
file |
diff |
annotate
|
| Sun, 23 Sep 2007 22:23:35 +0200 |
wenzelm |
added read_term_pattern/schematic/abbrev;
|
file |
diff |
annotate
|
| Sat, 22 Sep 2007 17:45:57 +0200 |
wenzelm |
removed obsolete set_expand_abbrevs (superceded by mode_abbrev);
|
file |
diff |
annotate
|
| Mon, 17 Sep 2007 16:36:41 +0200 |
wenzelm |
avoid direct access to print_mode;
|
file |
diff |
annotate
|
| Sat, 01 Sep 2007 18:17:44 +0200 |
wenzelm |
removed unused join_mode;
|
file |
diff |
annotate
|
| Sat, 01 Sep 2007 15:47:04 +0200 |
wenzelm |
removed obsolete read/cert variations (cf. Syntax.read/check);
|
file |
diff |
annotate
|
| Fri, 31 Aug 2007 23:17:25 +0200 |
wenzelm |
reject_vars: accept type-inference params;
|
file |
diff |
annotate
|
| Fri, 31 Aug 2007 18:46:35 +0200 |
wenzelm |
export various inner syntax modes;
|
file |
diff |
annotate
|
| Thu, 30 Aug 2007 22:35:40 +0200 |
wenzelm |
added join_mode;
|
file |
diff |
annotate
|
| Thu, 30 Aug 2007 15:04:48 +0200 |
wenzelm |
moved type_mode to type.ML;
|
file |
diff |
annotate
|
| Tue, 21 Aug 2007 20:05:38 +0200 |
wenzelm |
added inner syntax mode, includes former type_mode and is_stmt;
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 23:41:40 +0200 |
wenzelm |
inner syntax: added parse_term/prop;
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 20:44:03 +0200 |
wenzelm |
prepare_dummies: NAMED_CRITICAL;
|
file |
diff |
annotate
|
| Tue, 14 Aug 2007 23:23:06 +0200 |
wenzelm |
added implicit type mode (cf. Type.mode);
|
file |
diff |
annotate
|
| Fri, 27 Jul 2007 21:55:22 +0200 |
wenzelm |
get_thm etc.: map empty name to dummy_thm;
|
file |
diff |
annotate
|
| Mon, 23 Jul 2007 14:06:12 +0200 |
wenzelm |
marked some CRITICAL sections (for multithreading);
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 00:02:04 +0200 |
wenzelm |
tuned msg;
|
file |
diff |
annotate
|
| Sat, 02 Jun 2007 18:05:33 +0200 |
wenzelm |
moved specific target/local_abbrev to theory_target.ML;
|
file |
diff |
annotate
|