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;
2006-12-29 wenzelm 2006-12-29 replaced Sign.classes by Sign.all_classes (topologically sorted);
2006-12-29 aspinall 2006-12-29 Enable new Proof General code again after SML/NJ compatibility fixes by Florian.
2006-12-29 aspinall 2006-12-29 Typo in last commit
2006-12-29 haftmann 2006-12-29 explicit construction of operational classes
2006-12-29 haftmann 2006-12-29 added handling for explicit classrel witnesses
2006-12-29 haftmann 2006-12-29 ``classes`` now returns classes in topological order
2006-12-29 haftmann 2006-12-29 dropped some bookkeeping
2006-12-29 haftmann 2006-12-29 simplified class_package
2006-12-29 wenzelm 2006-12-29 use_ml: reverted to simple output (Poly/ML changed);
2006-12-28 haftmann 2006-12-28 removed private files
2006-12-28 wenzelm 2006-12-28 tuned;
2006-12-28 wenzelm 2006-12-28 removed nospaces (Char.isSpace does not conform to Isabelle conventions);
2006-12-28 wenzelm 2006-12-28 tuned msg;
2006-12-28 wenzelm 2006-12-28 inlined nospaces (from library.ML);
2006-12-28 haftmann 2006-12-28 added
2006-12-27 haftmann 2006-12-27 some clarifications
2006-12-27 haftmann 2006-12-27 different handling of type variable names
2006-12-27 haftmann 2006-12-27 added split
2006-12-27 haftmann 2006-12-27 fixed misleading error message
2006-12-27 haftmann 2006-12-27 dropped section header
2006-12-27 haftmann 2006-12-27 added OCaml code generation (without dictionaries)