| 2009-03-04 |
blanchet |
2009-03-04 |
Merge.
|
file | diff | annotate |
| 2009-03-04 |
blanchet |
2009-03-04 |
Merge.
|
file | diff | annotate |
| 2009-03-03 |
wenzelm |
2009-03-03 |
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;
minor tuning;
|
file | diff | annotate |
| 2009-03-03 |
wenzelm |
2009-03-03 |
Binding.str_of;
|
file | diff | annotate |
| 2009-02-27 |
wenzelm |
2009-02-27 |
eliminated NJ's List.nth;
|
file | diff | annotate |
| 2009-01-21 |
wenzelm |
2009-01-21 |
removed Ids;
|
file | diff | annotate |
| 2009-01-21 |
haftmann |
2009-01-21 |
binding is alias for Binding.T
|
file | diff | annotate |
| 2008-12-05 |
haftmann |
2008-12-05 |
Name.name_of -> Binding.base_name
|
file | diff | annotate |
| 2008-12-04 |
haftmann |
2008-12-04 |
cleaned up binding module and related code
|
file | diff | annotate |
| 2008-12-01 |
haftmann |
2008-12-01 |
new Binding module
|
file | diff | annotate |
| 2008-11-20 |
haftmann |
2008-11-20 |
dropped legacy naming code
|
file | diff | annotate |
| 2008-11-20 |
haftmann |
2008-11-20 |
using name bindings
|
file | diff | annotate |
| 2008-11-14 |
haftmann |
2008-11-14 |
namify and name_decl combinators
|
file | diff | annotate |
| 2008-09-03 |
wenzelm |
2008-09-03 |
declare_const: Name.binding, store/report position;
|
file | diff | annotate |
| 2008-08-27 |
wenzelm |
2008-08-27 |
type Properties.T;
|
file | diff | annotate |
| 2008-06-20 |
haftmann |
2008-06-20 |
type constructors now with markup
|
file | diff | annotate |
| 2008-06-19 |
wenzelm |
2008-06-19 |
moved get_sort to Isar/proof_context.ML;
removed obsolete read_def_typ, read_typ, read_typ_syntax, read_typ_abbrev;
|
file | diff | annotate |
| 2008-06-18 |
wenzelm |
2008-06-18 |
removed obsolete term reading operations (cf. old_goals.ML for legacy emulations);
|
file | diff | annotate |
| 2008-06-14 |
wenzelm |
2008-06-14 |
certify_term: reject qualified frees;
|
file | diff | annotate |
| 2008-06-13 |
wenzelm |
2008-06-13 |
map_const: soft version, no failure here;
|
file | diff | annotate |
| 2008-05-23 |
wenzelm |
2008-05-23 |
add constants: set Markup.theory_nameN in tags;
|
file | diff | annotate |
| 2008-05-18 |
wenzelm |
2008-05-18 |
moved global pretty/string_of functions from Sign to Syntax;
|
file | diff | annotate |
| 2008-05-17 |
wenzelm |
2008-05-17 |
added pretty_global flag;
|
file | diff | annotate |
| 2008-04-17 |
wenzelm |
2008-04-17 |
token translations: context dependent, result Pretty.T;
|
file | diff | annotate |
| 2008-04-15 |
wenzelm |
2008-04-15 |
removed obsolete SIGN_THEORY -- no name aliases in structure Theory;
simplified hide_XXX interfaces;
moved hide_names to isar_cmd.ML;
|
file | diff | annotate |
| 2008-04-13 |
wenzelm |
2008-04-13 |
tsig: removed unnecessary universal witness;
|
file | diff | annotate |
| 2008-04-12 |
wenzelm |
2008-04-12 |
rep_cterm/rep_thm: no longer dereference theory_ref;
removed obsolete compression;
|
file | diff | annotate |
| 2008-03-14 |
haftmann |
2008-03-14 |
added mk_const functions
|
file | diff | annotate |
| 2007-11-27 |
wenzelm |
2007-11-27 |
standard_parse_term: check ambiguous results without changing the result yet;
|
file | diff | annotate |
| 2007-11-23 |
haftmann |
2007-11-23 |
separated typedecl module, providing typedecl command with interpretation
|
file | diff | annotate |
| 2007-11-11 |
wenzelm |
2007-11-11 |
syntax operations: turned extend'' into update'' (absorb duplicates);
|
file | diff | annotate |
| 2007-11-10 |
wenzelm |
2007-11-10 |
notation: based on Syntax.update_const_gram (avoids duplicates);
|
file | diff | annotate |
| 2007-11-09 |
wenzelm |
2007-11-09 |
tyabbr/syntax/consts: replaced obsolete read_typ by Syntax.parse_typ/certify_typ;
|
file | diff | annotate |
| 2007-11-08 |
wenzelm |
2007-11-08 |
removed unused read_def_terms';
|
file | diff | annotate |
| 2007-11-07 |
wenzelm |
2007-11-07 |
removed obsolete Sign.read_tyname/const (cf. ProofContext);
|
file | diff | annotate |
| 2007-10-20 |
wenzelm |
2007-10-20 |
no_variables: tuned error msg;
|
file | diff | annotate |
| 2007-10-17 |
wenzelm |
2007-10-17 |
removed unused set_policy;
|
file | diff | annotate |
| 2007-10-16 |
wenzelm |
2007-10-16 |
add_abbrev: removed Logic.legacy_varifyT, do not unvarify result (again);
added revert_abbrev;
|
file | diff | annotate |
| 2007-10-15 |
wenzelm |
2007-10-15 |
renamed Consts.the_declaration to Consts.the_type;
|
file | diff | annotate |
| 2007-10-13 |
wenzelm |
2007-10-13 |
add_abbrevs: unvarify result;
|
file | diff | annotate |
| 2007-10-11 |
wenzelm |
2007-10-11 |
dest/cert_def: replaced Pretty.pp by explicit Proof.context;
|
file | diff | annotate |
| 2007-10-11 |
wenzelm |
2007-10-11 |
tuned;
|
file | diff | annotate |
| 2007-10-11 |
wenzelm |
2007-10-11 |
replaced Sign.add_consts_authentic by Sign.declare_const;
|
file | diff | annotate |
| 2007-10-10 |
wenzelm |
2007-10-10 |
generalized notation interface (add or del);
|
file | diff | annotate |
| 2007-10-09 |
wenzelm |
2007-10-09 |
generic Syntax.pretty/string_of operations;
existing pretty_term = Syntax.pretty_term o ProofContext.init etc.;
removed pretty_classrel/arity (cf. Syntax/syntax.ML);
|
file | diff | annotate |
| 2007-09-30 |
wenzelm |
2007-09-30 |
add_consts_authentic/add_abbrev: tags (Markup.property list);
tuned signature;
|
file | diff | annotate |
| 2007-09-29 |
wenzelm |
2007-09-29 |
removed obsolete external interface add_const_constraint;
removed redundant const_constraint;
renamed add_const_constraint_i to add_const_constraint;
|
file | diff | annotate |
| 2007-09-26 |
wenzelm |
2007-09-26 |
added minimize_sort, complete_sort;
|
file | diff | annotate |
| 2007-09-25 |
wenzelm |
2007-09-25 |
Syntax.parse/check/read;
|
file | diff | annotate |
| 2007-09-22 |
wenzelm |
2007-09-22 |
certify': proper do_expand argument (which observes force_expand consts) instead of home-grown normalize;
|
file | diff | annotate |
| 2007-09-01 |
wenzelm |
2007-09-01 |
read_def_terms: replaced full Syntax.check_typs by certify_typ, to workaround problems with illegal schematic type vars;
|
file | diff | annotate |
| 2007-08-30 |
wenzelm |
2007-08-30 |
infer_types: general check_typs instead of Type.cert_typ_mode;
|
file | diff | annotate |
| 2007-08-20 |
wenzelm |
2007-08-20 |
read_def_terms: moved disambig to syntax.ML;
|
file | diff | annotate |
| 2007-08-14 |
wenzelm |
2007-08-14 |
replaced certify_typ_syntax/abbrev by certify_typ_mode;
removed obsolete read_sort', read_typ', read_typ_syntax', read_typ_abbrev';
|
file | diff | annotate |
| 2007-08-14 |
wenzelm |
2007-08-14 |
PrimitiveDefs.dest_def;
Syntax.standard_read;
|
file | diff | annotate |
| 2007-08-12 |
wenzelm |
2007-08-12 |
read_def_terms': restrict scope of disambiguation to individual term;
|
file | diff | annotate |
| 2007-08-03 |
wenzelm |
2007-08-03 |
certify: no check_thy here;
|
file | diff | annotate |
| 2007-07-24 |
wenzelm |
2007-07-24 |
moved exception capture/release to structure Exn;
|
file | diff | annotate |
| 2007-07-09 |
wenzelm |
2007-07-09 |
type output = string indicates raw system output;
|
file | diff | annotate |
| 2007-07-07 |
wenzelm |
2007-07-07 |
simplified pretty token metric: type int;
|
file | diff | annotate |