2005-12-17 wenzelm 2005-12-17 sort_distinct;
2005-12-17 wenzelm 2005-12-17 added sort_distinct; removed obsolete unique_strings;
2005-12-16 urbanc 2005-12-16 added container-lemma fresh_eqvt (definition: container-lemma contains all instantiations of a lemma from the general theory)
2005-12-16 urbanc 2005-12-16 I think the earlier version was completely broken (not sure about this one)
2005-12-16 urbanc 2005-12-16 tuned more proofs
2005-12-16 nipkow 2005-12-16 new lemmas
2005-12-16 haftmann 2005-12-16 re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-16 haftmann 2005-12-16 re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-16 paulson 2005-12-16 hashing to eliminate the output of duplicate clauses
2005-12-16 paulson 2005-12-16 hash tables from SML/NJ
2005-12-16 haftmann 2005-12-16 re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-15 urbanc 2005-12-15 there was a small error in the last commit - fixed now
2005-12-15 urbanc 2005-12-15 tuned more proof and added in-file documentation
2005-12-15 wenzelm 2005-12-15 improved proofs;
2005-12-15 wenzelm 2005-12-15 acc_induct: proper tags;
2005-12-15 wenzelm 2005-12-15 removed obsolete/unused setup_induction;
2005-12-15 urbanc 2005-12-15 tuned the proof of transitivity/narrowing
2005-12-15 paulson 2005-12-15 No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are deleted; any positive occurrence of HOL.type kills the entire clause.
2005-12-15 urbanc 2005-12-15 made further tunings
2005-12-15 mengj 2005-12-15 Added functions to test equivalence between clauses.
2005-12-14 webertj 2005-12-14 ex/Sudoku.thy
2005-12-14 paulson 2005-12-14 deleted redundant (looping!) simprule
2005-12-14 paulson 2005-12-14 modified example for new clauses
2005-12-14 paulson 2005-12-14 removal of some redundancies (e.g. one-point-rules) in clause production
2005-12-14 paulson 2005-12-14 removed unused function repeat_RS
2005-12-14 mengj 2005-12-14 Changed literals' ordering and the functions for sorting literals.
2005-12-14 mengj 2005-12-14 1. changed fol_type, it's not a string type anymore. 2. sort literals in clauses.
2005-12-14 mengj 2005-12-14 changed ATP input files' names and location.
2005-12-13 wenzelm 2005-12-13 Potentially infinite lists as greatest fixed-point.
2005-12-13 wenzelm 2005-12-13 Provers/induct: coinduct; HOL/Library: theory Coinductive_List;
2005-12-13 wenzelm 2005-12-13 tuned proofs;
2005-12-13 wenzelm 2005-12-13 added HOL/Library/Coinductive_List.thy;
2005-12-13 urbanc 2005-12-13 added a fresh_left lemma that contains all instantiation for the various atom-types.
2005-12-13 urbanc 2005-12-13 initial commit (not to be seen by the public)
2005-12-13 chaieb 2005-12-13 simpset for computation in raw_arith_tac added just as comment, nothing changed!
2005-12-13 chaieb 2005-12-13 deals with Suc in mod expressions
2005-12-13 wenzelm 2005-12-13 Poplog/pml provides a proper print function already!
2005-12-13 paulson 2005-12-13 meson no longer does these examples
2005-12-13 paulson 2005-12-13 now generates the name "append"
2005-12-13 paulson 2005-12-13 removal of functional reflexivity axioms
2005-12-13 berghofe 2005-12-13 list_of_indset now also generates code for set type.
2005-12-12 haftmann 2005-12-12 added generic name mangler
2005-12-12 haftmann 2005-12-12 improvement in eq handling
2005-12-12 haftmann 2005-12-12 improvements in class and eq handling
2005-12-12 haftmann 2005-12-12 added dummy 'print' to non-polyml systems
2005-12-11 urbanc 2005-12-11 ISAR-fied some proofs
2005-12-11 urbanc 2005-12-11 completed the sn proof and changed the manual accordingly
2005-12-10 urbanc 2005-12-10 changed the types in accordance with Florian's changes
2005-12-09 haftmann 2005-12-09 substantial improvements for class code generation
2005-12-09 haftmann 2005-12-09 improved extraction interface
2005-12-09 urbanc 2005-12-09 tuned
2005-12-09 haftmann 2005-12-09 oriented result pairs in PureThy
2005-12-08 wenzelm 2005-12-08 tuned;
2005-12-08 wenzelm 2005-12-08 removed Syntax.deskolem;
2005-12-08 wenzelm 2005-12-08 swap: no longer pervasive;
2005-12-08 wenzelm 2005-12-08 replaced swap by contrapos_np;
2005-12-08 wenzelm 2005-12-08 tuned proofs;
2005-12-08 wenzelm 2005-12-08 Cla.swap;
2005-12-08 wenzelm 2005-12-08 removed hint for Classical.swap, which is not really user-level anyway;
2005-12-08 wenzelm 2005-12-08 tuned sources and proofs