2005-11-16 paulson 2005-11-16 new version of "tryres" allowing multiple unifiers (apparently needed for Skolemization of higher-order theorems)
2005-11-16 wenzelm 2005-11-16 pgmlsymbolson: append Symbol.xsymbolsN at end!
2005-11-15 wenzelm 2005-11-15 better no -d option;
2005-11-15 haftmann 2005-11-15 added generic transformators
2005-11-14 paulson 2005-11-14 removal of is_hol
2005-11-14 haftmann 2005-11-14 added module system
2005-11-14 haftmann 2005-11-14 added modules for code generator generation two, not operational yet
2005-11-14 haftmann 2005-11-14 class_package - operational view on type classes
2005-11-14 haftmann 2005-11-14 string_of_alist - convenient q'n'd printout function
2005-11-14 wenzelm 2005-11-14 support for polyml-4.2.0;
2005-11-14 haftmann 2005-11-14 new syntax for class_package
2005-11-14 wenzelm 2005-11-14 added const_instance;
2005-11-14 wenzelm 2005-11-14 added instance;
2005-11-14 wenzelm 2005-11-14 added ML-Systems/polyml-4.1.4-patch.ML, ML-Systems/polyml-4.2.0.ML;
2005-11-14 wenzelm 2005-11-14 Compatibility wrapper for Poly/ML 4.2.0.
2005-11-14 wenzelm 2005-11-14 tuned;
2005-11-14 urbanc 2005-11-14 added a few equivariance lemmas (they need to be automated eventually)
2005-11-13 urbanc 2005-11-13 changed the HOL_basic_ss back and selectively added simp_thms and triv_forall_equality. (Otherwise the goals would have been simplified too much)
2005-11-13 urbanc 2005-11-13 exchanged HOL_ss for HOL_basic_ss in the simplification part. Otherwise the case where the context is instantiated with unit leads to vacuous quantifiers, such as ALL a. A
2005-11-11 chaieb 2005-11-11 a proof step corrected due to the changement in the presburger method.
2005-11-11 chaieb 2005-11-11 old argument "abs" is replaced by "no_abs". Abstraction is turned on by default.
2005-11-11 huffman 2005-11-11 add header
2005-11-10 wenzelm 2005-11-10 tuned proofs;
2005-11-10 wenzelm 2005-11-10 moved find_free to term.ML;
2005-11-10 wenzelm 2005-11-10 guess: Seq.hd; Term.find_free;
2005-11-10 wenzelm 2005-11-10 guess: Toplevel.proof;
2005-11-10 wenzelm 2005-11-10 added find_free (from Isar/proof_context.ML);
2005-11-10 wenzelm 2005-11-10 curried multiply;
2005-11-10 wenzelm 2005-11-10 induct method: fixes; tuned;
2005-11-10 wenzelm 2005-11-10 uncurried Consts.typargs;
2005-11-10 wenzelm 2005-11-10 renamed Thm.cgoal_of to Thm.cprem_of;
2005-11-10 paulson 2005-11-10 duplicate axioms in ATP linkup, and general fixes
2005-11-10 paulson 2005-11-10 tidying
2005-11-10 urbanc 2005-11-10 called the induction principle "unsafe" instead of "test".
2005-11-09 paulson 2005-11-09 Skolemization by inference, but not quite finished
2005-11-09 wenzelm 2005-11-09 Explicit data structures for some Isar language elements.
2005-11-09 wenzelm 2005-11-09 tuned;
2005-11-09 wenzelm 2005-11-09 tvars_intr_list: natural argument order;
2005-11-09 wenzelm 2005-11-09 moved datatype elem to element.ML; removed unused imports function;
2005-11-09 wenzelm 2005-11-09 P.context_element, P.locale_element;
2005-11-09 wenzelm 2005-11-09 Element.context;
2005-11-09 wenzelm 2005-11-09 use existing exeption Empty;
2005-11-09 wenzelm 2005-11-09 avoid code redundancy; tuned comments;
2005-11-09 wenzelm 2005-11-09 tuned comments;
2005-11-09 wenzelm 2005-11-09 removed obsolete term set operations;
2005-11-09 wenzelm 2005-11-09 P.locale_element;
2005-11-09 wenzelm 2005-11-09 added fold_terms; added tfrees_of, frees_of; tvars_intr_list: natural argument order;
2005-11-09 wenzelm 2005-11-09 added Isar/element.ML;
2005-11-09 wenzelm 2005-11-09 Thm.varifyT': natural argument order;
2005-11-09 haftmann 2005-11-09 added join function
2005-11-08 haftmann 2005-11-08 allowing indentation of 'theory' keyword
2005-11-08 wenzelm 2005-11-08 simplified after_qed;
2005-11-08 wenzelm 2005-11-08 avoid prove_plain, export_plain, simplified after_qed; witness = term * thm, i.e. the original proposition with a protected fact (this achieves reliable discharge and allows facts to be slightly more general/normalized); internal assume/prove/conclude/satisfy_protected handle witness pairs accordingly; ObjectLogic.ensure_propT;
2005-11-08 wenzelm 2005-11-08 removed export_plain; (some_)fact_tac: Drule.incr_indexes;
2005-11-08 wenzelm 2005-11-08 renamed assert_prop to ensure_prop;
2005-11-08 wenzelm 2005-11-08 renamed goals.ML to old_goals.ML; inline Drule.impose_hyps;
2005-11-08 wenzelm 2005-11-08 export compose_hhf; removed obsolete norm_hhf_plain; tuned;
2005-11-08 wenzelm 2005-11-08 removed impose_hyps, satisfy_hyps; tuned;
2005-11-08 wenzelm 2005-11-08 const args: do not store variable names (unused);
2005-11-08 wenzelm 2005-11-08 renamed goals.ML to old_goals.ML;