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;