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