| 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
|