2005-12-22 nipkow 2005-12-22 new lemmas
2005-12-22 paulson 2005-12-22 Fixed a use of an outdated Substring function
2005-12-22 wenzelm 2005-12-22 tuned;
2005-12-22 wenzelm 2005-12-22 exh_casedist2: norm_hhf_eq;
2005-12-22 wenzelm 2005-12-22 added bicompose_no_flatten, which refrains from changing the shape of the new subgoals;
2005-12-22 wenzelm 2005-12-22 bicompose_proof: no_flatten;
2005-12-22 wenzelm 2005-12-22 conclude/SELECT: Thm.bicompose_no_flatten avoids unsolicited modification of result;
2005-12-22 wenzelm 2005-12-22 Transform mutual rule into projection.
2005-12-22 wenzelm 2005-12-22 added Provers/project_rule.ML
2005-12-22 wenzelm 2005-12-22 structure ProjectRule;
2005-12-22 wenzelm 2005-12-22 * induct: improved treatment of mutual goals and mutual rules;
2005-12-22 wenzelm 2005-12-22 updated auxiliary facts for induct method; removed dead code;
2005-12-22 wenzelm 2005-12-22 prop_tr': proper handling of aprop marked as bound;
2005-12-22 wenzelm 2005-12-22 consume: expand defs in prems of concls; added add_consumes; make/extract_cases: split cases consisting of meta-conjunctions; added mutual_rule;
2005-12-22 wenzelm 2005-12-22 cases: main is_proper flag; print_cases: show proper cases only;
2005-12-22 wenzelm 2005-12-22 auto cases: marked improper; tuned;
2005-12-22 wenzelm 2005-12-22 conjunction_tac: single goal;
2005-12-22 wenzelm 2005-12-22 CONJUNCTS2;
2005-12-22 wenzelm 2005-12-22 rule_context: numbered cases;
2005-12-22 wenzelm 2005-12-22 conjunction_tac: single goal; added CONJUNCTS2, precise_conjunction_tac; removed smart_conjunction_tac;
2005-12-22 wenzelm 2005-12-22 renamed imp_cong' to imp_cong_rule;
2005-12-22 wenzelm 2005-12-22 mk_conjunction: proper treatment of bounds; added dest_conjunction(s);
2005-12-22 wenzelm 2005-12-22 fixed has_internal; added is_internal; renamed imp_cong' to imp_cong_rule; uniform versions of forall_conv, concl_conv, prems_conv, conjunction_conv;
2005-12-22 wenzelm 2005-12-22 Tactic.precise_conjunction_tac;
2005-12-22 wenzelm 2005-12-22 added locale meta_conjunction_syntax and various conjunction rules;
2005-12-22 wenzelm 2005-12-22 simplified setup: removed dest_concls, local_impI, conjI; improved handling of simultaneous goals: split cases; simplified treatment of mutual rules, which are now specified as a list instead of object-level conjunction (cf. set/type/rule); moved join_rules to RuleCases.mutual_rule;
2005-12-22 wenzelm 2005-12-22 induct_rulify;
2005-12-22 wenzelm 2005-12-22 actually produce projected rules; *.inducts holds all projected rules;
2005-12-22 wenzelm 2005-12-22 *.inducts holds all projected rules;
2005-12-22 wenzelm 2005-12-22 tuned;
2005-12-22 wenzelm 2005-12-22 tuned induct proofs;
2005-12-22 wenzelm 2005-12-22 mutual induct with *.inducts;
2005-12-22 wenzelm 2005-12-22 wf_induct_rule: consumes 1;
2005-12-22 wenzelm 2005-12-22 structure ProjectRule; updated auxiliary facts for induct method; tuned proofs;
2005-12-22 wenzelm 2005-12-22 updated auxiliary facts for induct method;
2005-12-21 haftmann 2005-12-21 slight improvements
2005-12-21 haftmann 2005-12-21 slight improvements in name handling
2005-12-21 haftmann 2005-12-21 slight refinements
2005-12-21 haftmann 2005-12-21 added eq_ord
2005-12-21 haftmann 2005-12-21 slight clean ups
2005-12-21 haftmann 2005-12-21 discontinued unflat in favour of burrow and burrow_split
2005-12-21 paulson 2005-12-21 new hash table module in HOL/Too/s
2005-12-21 paulson 2005-12-21 modified suffix for [iff] attribute
2005-12-21 paulson 2005-12-21 removed or modified some instances of [iff]
2005-12-20 wenzelm 2005-12-20 tuned;
2005-12-20 haftmann 2005-12-20 added .cvsignore
2005-12-20 haftmann 2005-12-20 removed improper .cvsignore
2005-12-20 haftmann 2005-12-20 removed superfluos is_prefix functions
2005-12-20 haftmann 2005-12-20 resolved shadowing of Library.find_first
2005-12-20 haftmann 2005-12-20 removed infix prefix, introduces burrow
2005-12-20 mengj 2005-12-20 Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
2005-12-20 mengj 2005-12-20 Added functions for fol_type; also put some functions to the signature, used by ResHolClause.
2005-12-19 urbanc 2005-12-19 made the changes according to Florian's re-arranging of tuples (everything up to 19th December).
2005-12-19 urbanc 2005-12-19 added proofs to show that every atom-kind combination is in the respective finite-support class (now have to adjust the files according to Florian's changes)
2005-12-19 urbanc 2005-12-19 added thms to perm_compose (so far only composition theorems were included where the type of the permutation was equal)
2005-12-19 urbanc 2005-12-19 tuned one comment
2005-12-19 urbanc 2005-12-19 fixed a bug that occured when more than one atom-type is declared.
2005-12-19 nipkow 2005-12-19 fixed proof
2005-12-18 urbanc 2005-12-18 more cleaning up - this time of the cp-instance proofs
2005-12-18 urbanc 2005-12-18 improved the finite-support proof added finite support proof for options (I am surprised that one does not need more fs-proofs; at the moment only lists, products, units and atoms are shown to be finitely supported (of course also every nominal datatype is finitely supported)) deleted pt_bool_inst - not necessary because discrete types are treated separately in nominal_atoms