structure ProjectRule;

* induct: improved treatment of mutual goals and mutual rules;

updated auxiliary facts for induct method; removed dead code;

prop_tr': proper handling of aprop marked as bound;

consume: expand defs in prems of concls; added add_consumes; make/extract_cases: split cases consisting of meta-conjunctions; added mutual_rule;

cases: main is_proper flag; print_cases: show proper cases only;

auto cases: marked improper; tuned;

conjunction_tac: single goal;

CONJUNCTS2;

rule_context: numbered cases;

conjunction_tac: single goal; added CONJUNCTS2, precise_conjunction_tac; removed smart_conjunction_tac;

renamed imp_cong' to imp_cong_rule;

mk_conjunction: proper treatment of bounds; added dest_conjunction(s);

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.

ex/Sudoku.thy

deleted redundant (looping!) simprule

modified example for new clauses

removal of some redundancies (e.g. one-point-rules) in clause production

removed unused function repeat_RS

Changed literals' ordering and the functions for sorting literals.

1. changed fol_type, it's not a string type anymore. 2. sort literals in clauses.

changed ATP input files' names and location.

Potentially infinite lists as greatest fixed-point.

Provers/induct: coinduct; HOL/Library: theory Coinductive_List;

tuned proofs;

added HOL/Library/Coinductive_List.thy;

added a fresh_left lemma that contains all instantiation for the various atom-types.

initial commit (not to be seen by the public)

simpset for computation in raw_arith_tac added just as comment, nothing changed!

deals with Suc in mod expressions

Poplog/pml provides a proper print function already!

meson no longer does these examples

now generates the name "append"

removal of functional reflexivity axioms

list_of_indset now also generates code for set type.

added generic name mangler

improvement in eq handling

improvements in class and eq handling

added dummy 'print' to non-polyml systems

ISAR-fied some proofs

completed the sn proof and changed the manual accordingly

changed the types in accordance with Florian's changes

substantial improvements for class code generation

improved extraction interface

tuned

oriented result pairs in PureThy

tuned;

removed Syntax.deskolem;

swap: no longer pervasive;

replaced swap by contrapos_np;

tuned proofs;

Cla.swap;

removed hint for Classical.swap, which is not really user-level anyway;

tuned sources and proofs

Classical.swap;

* HOL: Theorem 'swap' is no longer bound at the ML top-level.

Adapted to new type of PureThy.add_defs_i.

replaced swap by Classical.swap;

avoid unportable tail;

tuned

removed thms 'swap' and 'nth_map' from ML toplevel