2007-01-04 haftmann 2007-01-04 fixed output
2007-01-04 haftmann 2007-01-04 different handling of eta expansion
2007-01-04 haftmann 2007-01-04 eta-expansion now only to common maximum number of arguments
2007-01-04 haftmann 2007-01-04 clarified code
2007-01-04 haftmann 2007-01-04 more term examples
2007-01-04 haftmann 2007-01-04 eliminated Option.app
2007-01-04 webertj 2007-01-04 constants are unfolded, universal quantifiers are stripped, some minor changes
2007-01-03 aspinall 2007-01-03 Fix error reporting in Emacs to also match Isar command failure exactly.
2007-01-03 aspinall 2007-01-03 Use Isar toplevel print_exn_fn for generating error responses instead of Output.error_msg.
2007-01-03 aspinall 2007-01-03 Expose command failure recovery code for top level.
2007-01-03 aspinall 2007-01-03 Selected functions from syntax module
2007-01-03 paulson 2007-01-03 x-symbol is no longer switched off in the ATP linkup
2007-01-03 paulson 2007-01-03 Improvements to proof reconstruction. Now "fixes" is inserted
2007-01-03 paulson 2007-01-03 Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
2007-01-03 paulson 2007-01-03 first version of structured proof reconstruction
2007-01-02 wenzelm 2007-01-02 Morphism.fact;
2007-01-02 wenzelm 2007-01-02 Term.lambda: abstract over arbitrary closed terms;
2006-12-31 aspinall 2006-12-31 Add standalone file to help porters
2006-12-31 aspinall 2006-12-31 Quote arguments in PGIP exceptions. Tune comment.
2006-12-31 aspinall 2006-12-31 Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
2006-12-31 aspinall 2006-12-31 Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
2006-12-30 wenzelm 2006-12-30 removed dead code;
2006-12-30 wenzelm 2006-12-30 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;
2006-12-30 wenzelm 2006-12-30 removed conditional combinator; refrain from setting ml_prompts again; tuned init;
2006-12-30 wenzelm 2006-12-30 refrain from setting ml_prompts again;
2006-12-30 wenzelm 2006-12-30 removed misleading OuterLex.eq_token;
2006-12-30 wenzelm 2006-12-30 pretty_statement: more careful handling of name_hint;
2006-12-30 wenzelm 2006-12-30 added has_name_hint; name_thm: more careful pre-naming;
2006-12-30 wenzelm 2006-12-30 removed obsolete name_hint handling;
2006-12-30 wenzelm 2006-12-30 removed conditional combinator;
2006-12-30 wenzelm 2006-12-30 removed obsolete support for polyml-4.9.1;
2006-12-30 wenzelm 2006-12-30 * Proof General: proper undo of final 'end'; discontinued Isabelle/classic;
2006-12-30 wenzelm 2006-12-30 inform_file_processed: Toplevel.init_empty;
2006-12-30 wenzelm 2006-12-30 refined notion of empty toplevel, admits undo of 'end'; added undo_exit, init_empty, init_state; removed unused toplevel, reset; tuned;
2006-12-30 wenzelm 2006-12-30 Toplevel.init_state;
2006-12-30 wenzelm 2006-12-30 removed obsolete 'clear_undos';
2006-12-30 wenzelm 2006-12-30 removed obsolete clear_undos_theory; undo/cannot_undo: proper undo of 'end';
2006-12-29 haftmann 2006-12-29 major restructurings
2006-12-29 haftmann 2006-12-29 cleanup
2006-12-29 haftmann 2006-12-29 improved print of constructors in OCaml
2006-12-29 haftmann 2006-12-29 changed syntax for axclass attach
2006-12-29 wenzelm 2006-12-29 removed obsolete cond_add_path;
2006-12-29 wenzelm 2006-12-29 removed obsolete context_thy etc.;
2006-12-29 wenzelm 2006-12-29 removed obsolete init_pgip; removed obsolete redo, context_thy etc.;
2006-12-29 wenzelm 2006-12-29 removed obsolete init_context;
2006-12-29 wenzelm 2006-12-29 obsolete (cf. ProofGeneral/proof_general_emacs.ML);
2006-12-29 wenzelm 2006-12-29 tuned;
2006-12-29 wenzelm 2006-12-29 signed_string_of_int;
2006-12-29 wenzelm 2006-12-29 added proper header;
2006-12-29 wenzelm 2006-12-29 added signed_string_of_int (pruduces proper - instead of SML's ~);
2006-12-29 wenzelm 2006-12-29 removed obsolete proof_general.ML;
2006-12-29 wenzelm 2006-12-29 minor tuning;
2006-12-29 wenzelm 2006-12-29 tuned specifications/proofs;
2006-12-29 wenzelm 2006-12-29 replaced Sign.classes by Sign.all_classes (topologically sorted); prefer structure Sign over Sorts; renamed Sorts.project to Sorts.subalgebra;
2006-12-29 wenzelm 2006-12-29 renamed Graph.project to Graph.subgraph;
2006-12-29 wenzelm 2006-12-29 replaced Sign.classes by Sign.all_classes (topologically sorted); prefer structure Sign over Sorts;
2006-12-29 wenzelm 2006-12-29 renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
2006-12-29 wenzelm 2006-12-29 Sorts.minimal_classes;
2006-12-29 wenzelm 2006-12-29 classes: more direct way to achieve topological sorting; renamed classes to all_classes; added minimal_classes; renamed project to subalgebra, tuned;
2006-12-29 wenzelm 2006-12-29 replaced classes by all_classes (topologically sorted); added minimal_classes;