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

improved serialization of classes to haskell

improved class handling

added 'dig' combinator

re-oriented some result tuples in PureThy

Added more functions for new type embedding of HOL clauses.

Added new type embedding methods for translating HOL clauses.

added code to say that discrete types (nat, bool, char) are instances of cp_*_*.

tuned

transitivity should be now in a reasonable state. But Markus has to have a look at some of the advanced features.

tuned

ISAR-fied two proofs

Adapted to new type of store_thmss(_atts).

Added store_thmss_atts to signature again.

tuned

tuned

tuned

added an Isar-proof for the abs_ALL lemma

tuning

defines: beta/eta contract lhs; replaced type_syntax by mixfix_type, which handles binders as well;

asts_to_terms: builtin free_fixed translation makes local binders work properly;