fixed has_internal; added is_internal; renamed imp_cong' to imp_cong_rule; uniform versions of forall_conv, concl_conv, prems_conv, conjunction_conv;

Tactic.precise_conjunction_tac;

added locale meta_conjunction_syntax and various conjunction rules;

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;

induct_rulify;

actually produce projected rules; *.inducts holds all projected rules;

*.inducts holds all projected rules;

tuned;

tuned induct proofs;

mutual induct with *.inducts;

wf_induct_rule: consumes 1;

structure ProjectRule; updated auxiliary facts for induct method; tuned proofs;

updated auxiliary facts for induct method;

slight improvements

slight improvements in name handling

slight refinements

added eq_ord

slight clean ups

discontinued unflat in favour of burrow and burrow_split

new hash table module in HOL/Too/s

modified suffix for [iff] attribute

removed or modified some instances of [iff]

tuned;

added .cvsignore

removed improper .cvsignore

removed superfluos is_prefix functions

resolved shadowing of Library.find_first

removed infix prefix, introduces burrow

Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.

Added functions for fol_type; also put some functions to the signature, used by ResHolClause.

made the changes according to Florian's re-arranging of tuples (everything up to 19th December).

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)

added thms to perm_compose (so far only composition theorems were included where the type of the permutation was equal)

tuned one comment

fixed a bug that occured when more than one atom-type is declared.

fixed proof

more cleaning up - this time of the cp-instance proofs

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

improved the code for showing that a type is in the pt-axclass (I try to slowly overcome my incompetence with such ML-code).

simp del: empty_Collect_eq;

sort_distinct;

added sort_distinct; removed obsolete unique_strings;

added container-lemma fresh_eqvt (definition: container-lemma contains all instantiations of a lemma from the general theory)

I think the earlier version was completely broken (not sure about this one)

tuned more proofs

new lemmas

re-arranged tuples (theory * 'a) to ('a * theory) in Pure

re-arranged tuples (theory * 'a) to ('a * theory) in Pure

hashing to eliminate the output of duplicate clauses

hash tables from SML/NJ

re-arranged tuples (theory * 'a) to ('a * theory) in Pure

there was a small error in the last commit - fixed now

tuned more proof and added in-file documentation

improved proofs;

acc_induct: proper tags;

removed obsolete/unused setup_induction;

tuned the proof of transitivity/narrowing

No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are deleted; any positive occurrence of HOL.type kills the entire clause.

made further tunings

Added functions to test equivalence between clauses.