eta-expansion now only to common maximum number of arguments

clarified code

more term examples

eliminated Option.app

constants are unfolded, universal quantifiers are stripped, some minor changes

Fix error reporting in Emacs to also match Isar command failure exactly.

Use Isar toplevel print_exn_fn for generating error responses instead of Output.error_msg.

Expose command failure recovery code for top level.

Selected functions from syntax module

x-symbol is no longer switched off in the ATP linkup

Improvements to proof reconstruction. Now "fixes" is inserted

Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction

first version of structured proof reconstruction

Morphism.fact;

Term.lambda: abstract over arbitrary closed terms;

Add standalone file to help porters

Quote arguments in PGIP exceptions. Tune comment.

Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.

Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.

removed dead code;

removed conditional combinator; avoid handle _; showctxt: print_context (cf. local theory context); searchtheorems: proper find_theorems; refrain from setting ml_prompts again; tuned init_pgip;

removed conditional combinator; refrain from setting ml_prompts again; tuned init;

refrain from setting ml_prompts again;

removed misleading OuterLex.eq_token;

pretty_statement: more careful handling of name_hint;

added has_name_hint; name_thm: more careful pre-naming;

removed obsolete name_hint handling;

removed conditional combinator;

removed obsolete support for polyml-4.9.1;

* Proof General: proper undo of final 'end'; discontinued Isabelle/classic;

inform_file_processed: Toplevel.init_empty;

refined notion of empty toplevel, admits undo of 'end'; added undo_exit, init_empty, init_state; removed unused toplevel, reset; tuned;

Toplevel.init_state;

removed obsolete 'clear_undos';

removed obsolete clear_undos_theory; undo/cannot_undo: proper undo of 'end';

major restructurings

cleanup

improved print of constructors in OCaml

changed syntax for axclass attach

removed obsolete cond_add_path;

removed obsolete context_thy etc.;

removed obsolete init_pgip; removed obsolete redo, context_thy etc.;

removed obsolete init_context;

obsolete (cf. ProofGeneral/proof_general_emacs.ML);

tuned;

signed_string_of_int;

added proper header;

added signed_string_of_int (pruduces proper - instead of SML's ~);

removed obsolete proof_general.ML;

minor tuning;

tuned specifications/proofs;

replaced Sign.classes by Sign.all_classes (topologically sorted); prefer structure Sign over Sorts; renamed Sorts.project to Sorts.subalgebra;

renamed Graph.project to Graph.subgraph;

replaced Sign.classes by Sign.all_classes (topologically sorted); prefer structure Sign over Sorts;

renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;

Sorts.minimal_classes;

classes: more direct way to achieve topological sorting; renamed classes to all_classes; added minimal_classes; renamed project to subalgebra, tuned;

replaced classes by all_classes (topologically sorted); added minimal_classes;

replaced Sign.classes by Sign.all_classes (topologically sorted);

Enable new Proof General code again after SML/NJ compatibility fixes by Florian.