2005-12-01 ago wenzelm unfold_tac: static evaluation of simpset;
2005-12-01 ago wenzelm superceded by timestart|stop.bash;
2005-12-01 ago wenzelm cpu time = user + system;
2005-12-01 ago wenzelm replaced lib/scripts/showtime by more advanced lib/scripts/timestart|stop.bash;
2005-12-01 ago berghofe assoc_consts and assoc_types now check number of arguments in template.
2005-12-01 ago berghofe Added new component "sorts" to record datatype_info.
2005-12-01 ago wenzelm timestop - report timing based on environment (cf. timestart.bash);
2005-12-01 ago wenzelm timestart - setup bash environment for timing;
2005-12-01 ago berghofe Improved norm_proof to handle proofs containing term (type) variables
2005-12-01 ago paulson restoring the old status of subset_refl
2005-12-01 ago haftmann oriented pairs theory * 'a to 'a * theory
2005-12-01 ago urbanc initial cleanup to use the new induction method
2005-12-01 ago urbanc cleaned up further the proofs (diamond still needs work);
2005-12-01 ago urbanc changed "fresh:" to "avoiding:" and cleaned up the weakening example
2005-11-30 ago wenzelm match_bind(_i): return terms;
2005-11-30 ago wenzelm method 'fact': SIMPLE_METHOD, i.e. insert facts;
2005-11-30 ago wenzelm simulaneous 'def';
2005-11-30 ago urbanc added facilities to prove the pt and fs instances
2005-11-30 ago urbanc started to change the transitivity/narrowing case:
2005-11-30 ago urbanc changed everything until the interesting transitivity_narrowing
2005-11-30 ago haftmann minor improvements
2005-11-30 ago urbanc modified almost everything for the new nominal_induct
2005-11-30 ago berghofe Changed order of predicate arguments and quantifiers in strong induction rule.
2005-11-30 ago urbanc fixed the lemma where the new names generated by nominal_induct
2005-11-30 ago urbanc added one clause for substitution in the lambda-case and
2005-11-30 ago wenzelm added rename_params_rule: recover orginal fresh names in subgoals/cases;
2005-11-30 ago urbanc changed induction principle and everything to conform with the
2005-11-30 ago wenzelm fresh: frees instead of terms, rename corresponding params in rule;
2005-11-30 ago urbanc adapted to the new nominal_induction
2005-11-30 ago urbanc changed \<sim> of permutation equality to \<triangleq>
2005-11-30 ago wenzelm fresh_unit_elim and fresh_prod_elim -- for nominal_induct;
2005-11-30 ago huffman reimplement Case expression pattern matching to support lazy patterns
2005-11-30 ago huffman add definitions as defs, not axioms
2005-11-30 ago huffman changed section names
2005-11-30 ago huffman add xsymbol syntax for u type constructor
2005-11-30 ago huffman add constant unit_when
2005-11-30 ago wenzelm proper treatment of tuple/tuple_fun -- nest to the left!
2005-11-29 ago wenzelm moved nth_list to Pure/library.ML;
2005-11-29 ago wenzelm added nth_list;
2005-11-29 ago wenzelm added mk_split;
2005-11-29 ago urbanc changed the order of the induction variable and the context
2005-11-29 ago wenzelm reworked version with proper support for defs, fixes, fresh specification;
2005-11-29 ago haftmann added haskell serializer
2005-11-29 ago haftmann exported customized syntax interface
2005-11-29 ago berghofe Corrected atom class constraints in strong induction rule.
2005-11-29 ago urbanc made some of the theorem look-ups static (by using
2005-11-28 ago haftmann added (curried) fold2
2005-11-28 ago wenzelm added proof of measure_induct_rule;
2005-11-28 ago mengj Added flags for setting and detecting whether a problem needs combinators.
2005-11-28 ago mengj Only output types if !keep_types is true.
2005-11-28 ago mengj Added two functions for CNF translation, used by other files.
2005-11-28 ago mengj Added in four control flags for HOL and FOL translations.
2005-11-28 ago mengj Slight modification to trace information.
2005-11-28 ago mengj Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.
2005-11-28 ago mengj Only output arities and class relations if !ResClause.keep_types is true.
2005-11-28 ago urbanc some small tuning
2005-11-28 ago urbanc ISAR-fied two proofs about equality for abstraction functions.
2005-11-27 ago wenzelm * Provers/induct: obtain pattern;
2005-11-27 ago urbanc added an authors section (please let me know if somebody is left out or unhappy)
2005-11-27 ago urbanc some minor tunings