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.