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;

mixfix_args: 1 for binders; string_of_mixfix: proper output of binders;

removed fixed_tr: now handled in syntax module; replaced mixfix_typ by TypeInfer.mixfixT, which handles binders as well; def: beta/eta contract lhs;

added mixfixT; paramify_dummies: treat dummyT as well, tuned;

defs: beta/eta contract lhs;

abs_def: beta/eta contract lhs;

Added recdef congruence rules for bounded quantifiers and commonly used higher order functions.

various improvements

adjusted to improved code generator interface

added perhaps option combinator

adopted keyword for code generator

Factored out proof for normalization of applications (norm_list).

introduced new map2, fold

typo

simprocs: static evaluation of simpset;

tuned;

tuned msg;

ProofContext.lthms_containing: suppress obvious duplicates;

unfold_tac: static evaluation of simpset;

superceded by timestart|stop.bash;

cpu time = user + system;

replaced lib/scripts/showtime by more advanced lib/scripts/timestart|stop.bash;

assoc_consts and assoc_types now check number of arguments in template.

Added new component "sorts" to record datatype_info.

timestop - report timing based on environment (cf. timestart.bash);

timestart - setup bash environment for timing;

Improved norm_proof to handle proofs containing term (type) variables with same name but different types (sorts): Offending term (type) variables are replaced by dummy (T)Frees before applying the substitution.

restoring the old status of subset_refl

oriented pairs theory * 'a to 'a * theory

initial cleanup to use the new induction method

cleaned up further the proofs (diamond still needs work); changed "fresh:" to "avoiding:"

changed "fresh:" to "avoiding:" and cleaned up the weakening example

match_bind(_i): return terms; mk_def: simultaneous defs; prepare_dummies: produce globally unique indexnames;