removed duplicate abbreviations (implicit inheritance);

restored notation for less/less_eq (observe proper order of mixfix annotations!); simplified notation for greater/greater_eq, which is only used for input; removed duplicate abbreviations (implicit inheritance);

Document structure in pgip_markup.ML. Minor fixes.

Type alias for XML content

setup for polyml-5.0;

set DYLD_LIBRARY_PATH as well;

Fix typo. Some cleanup for XML attributes

Add dependency for new Emacs PG code

Support PGIP communication for preferences in Emacs mode.

more careful indexing of local facts;

* Pure: official theorem names and additional comments are now strictly separate.

thm/prf: separate official name vs. additional tags;

thm/prf: separate official name vs. additional tags; write_to_file: Path.T;

notes: added non-official name;

note_thmss: added kind tag and non-official name;

Add separate PG Emacs configuration

Include pgip markup module

Build instructions for new Proof General module [not yet activated]

Forward compatibility with new Proof General module.

New files.

Revamped Proof General interface.

Add parse_string for attribute values and other string content

added Ramsey.thy to Library imports, to include it in the daily builds

fixed definition syntax

theory Alloc no longer works -- quick_and_dirty;

converted legacy ML script;

Minor.

Add output function

Add string buffer getter. Add Rawtext constructor to allow XML-escaped strings in tree.

Type abbreviations for element args and attributes

meta_term_syntax: proper operation on untyped preterms;

generalized type signature of foldSet, fold

added some support for embedded terms;

TLA: converted legacy ML scripts;

non-exported syntax

made SML/NJ happy

slight cleanup in hologic.ML

some syntax cleanup

stripped some legacy bindings

Added missing "standard"

Deleted dead code

Fixed a MAJOR BUG in clause-counting: only Boolean equalities now count as iffs

notes: proper naming of thm proof, activated import_export_proof;

added full_name;

notes: more careful treatment of Goal.close_result; tuned;

note_thmss: refrain from closing the derivation here;

notes: proper import/export of proofs (still inactive); Goal.norm/close_result; tuned;

removed obsolete (export_)standard;

added mixfix';

added merge_list;

zero_var_indexes_inst: multiple terms; tuned;

Theory.merge_list;

qualified MetaSimplifier.norm_hhf(_protect);

added norm/close_result (supercede local_standard etc.);

added zero_var_indexes_list; removed local_standard (cf. Goal.norm/close_result); instantiate: more precise handling of indexes;

Goal.norm/close_result;

simplified syntax for 'definition', 'abbreviation';

*** bad commit -- reverted to previous version ***

removed export_standard_morphism; Assumption.assms_of: cterm;

simplified add_thmss; mark predicate definitions as internal;

added map/burrow_facts; exported name_multi, name_thm;

added INCR_COMP, COMP_INCR;

tuned;

reworked notes: towards proper import/export of proof terms; tuned;

removed export_standard_morphism;

renamed SIMPLE_METHOD' to SIMPLE_METHOD''; added simple version of SIMPLE_METHOD';

added export; removed find_def, expand_defs;

tuned spaces/comments;

simplified method setup; reactivated dead code;

simplified method setup;

simplified method setup; tuned oracle setup;

clauses sorted according to term order (significant speedup in some cases)

Assumption.assms_of: cterm; added tmp version of export_standard_facts;

Element.generalize_facts;

removed export_standard_morphism; Assumption.assms_of: cterm;

simplified add_thmss; mark predicate definitions as internal;

added facts_map; replaced export(_standard)_facts by generalize_facts; tuned;

added map/burrow_facts; exported name_multi, name_thm;

COMP_INCR;

added INCR_COMP, COMP_INCR;

assms_of: cterm;

simplified Logic.count_prems;

tuned proofs;

go back to fixed atbroy51, fix at-poly-e path settings

Removed the references for counting combinators. Instead they are counted in actual clauses.

added strict_subset

added add_fixed;

simplified '?' operator; defs: more robust transitivity proofs, expand target defs as well; tuned;

simplified '?' operator; note_thmss: no naming;

simplified '?' operator; added expand_defs;

added burrow_fact; no export of name_thms(s);

dest_term: strip_imp_concl;

simplified '?' operator;

Added in another function clause_name_of.

Goals in clause form are sent to the relevance filter.

Call the right inform_file_processed function on <closefile>

Tidied code. Bool constructor is not needed.

tidied code

outermost universal quantifiers are stripped

typo fixed

added the function for free variables of a lambda-term, which is a tad more difficult to define than capture-avoiding substitution

outermost universal quantifiers are stripped

adapted function definitions to new syntax

Adapted to new nominal_primrec command.

additional bookkeeping for class target

small syntax tuning

introduced Simpdata structure

added Trueprop_conv

restructured some proofs

tuned keyword setup for SML code generator

moved order arities for fun and bool to Fun/Orderings

removed HOL structure

adjusted syntax for internal code generation

Added nominal_primrec command.

Adapted to new nominal_primrec command.

Added nominal_primrec.ML

Implemented new "nominal_primrec" command for defining functions on nominal datatypes.

Additional information about nominal datatypes (descriptor, recursion equations etc.) is now stored in theory.

converted legacy ML scripts;

Remove add_master_files which stripped paths for retracted files. Emacs PG already supports full paths here.