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