2009-11-02 wenzelm 2009-11-02 modernized structure Local_Syntax;
2009-11-02 wenzelm 2009-11-02 modernized structure AutoBind;
2009-11-02 wenzelm 2009-11-02 modernized structure Primitive_Defs;
2009-11-02 wenzelm 2009-11-02 modernized structure Simple_Syntax;
2009-11-02 wenzelm 2009-11-02 modernized structure Context_Position;
2009-11-02 wenzelm 2009-11-02 observe usual naming conventions;
2009-11-02 krauss 2009-11-02 find_theorems: respect conceal flag
2009-11-02 wenzelm 2009-11-02 DEEPEN: all tracing is subject to trace_DEEPEN (NB: Proof General tends to "popup" tracing output);
2009-11-02 wenzelm 2009-11-02 back to warning -- Proof General tends to "popup" tracing output;
2009-11-02 boehmes 2009-11-02 split parsing of counterexamples from translation into terms (avoids Term.dummyT and ill-typed terms)
2009-11-02 bulwahn 2009-11-02 merged
2009-10-31 bulwahn 2009-10-31 predicate compiler creates code equations for predicates with full mode
2009-10-30 bulwahn 2009-10-30 renamed rpred to random
2009-11-01 wenzelm 2009-11-01 Rules that characterize functional/relational specifications.
2009-11-01 wenzelm 2009-11-01 adapted Item_Net; tuned;
2009-11-01 wenzelm 2009-11-01 allow multi-index; more scalable merge; renamed delete to remove, and insert to update (standard naming conventions); tuned;
2009-11-01 wenzelm 2009-11-01 added insert_safe, delete_safe variants;
2009-11-01 wenzelm 2009-11-01 tuned signature;
2009-11-01 wenzelm 2009-11-01 modernized structure Context_Rules;
2009-11-01 wenzelm 2009-11-01 modernized structure Rule_Cases;
2009-10-30 haftmann 2009-10-30 merged
2009-10-30 haftmann 2009-10-30 dedicated theory for loading numeral simprocs
2009-10-30 haftmann 2009-10-30 set Pure theory name properly
2009-10-30 haftmann 2009-10-30 tuned code setup
2009-10-30 wenzelm 2009-10-30 some notes on SPASS 3.0 distribution;
2009-10-30 haftmann 2009-10-30 merged
2009-10-30 haftmann 2009-10-30 combined former theories Divides and IntDiv to one theory Divides
2009-10-30 haftmann 2009-10-30 tuned variable names of bindings; conceal predicate constants
2009-10-30 haftmann 2009-10-30 dedicated theory for loading numeral simprocs
2009-10-30 haftmann 2009-10-30 moved some div/mod lemmas to theory Divides
2009-10-30 haftmann 2009-10-30 tuned proof
2009-10-30 haftmann 2009-10-30 moved Commutative_Ring into session Decision_Procs
2009-10-30 boehmes 2009-10-30 abstract over variables in reversed order (application uses given order)
2009-10-30 boehmes 2009-10-30 disable printing of unparsed counterexamples for CVC3 and Yices
2009-10-30 boehmes 2009-10-30 pattern are separated only by spaces (no comma)
2009-10-30 wenzelm 2009-10-30 back to polyml-svn -- performance impact is minimal, slowdown was caused by accumulated cruft of long-running Mac OS;
2009-10-30 krauss 2009-10-30 less verbose termination tactics
2009-10-30 krauss 2009-10-30 less verbose inductive invocation
2009-10-30 krauss 2009-10-30 tuned
2009-10-30 krauss 2009-10-30 absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
2009-10-29 wenzelm 2009-10-29 merged
2009-10-29 wenzelm 2009-10-29 recovered from 7a1f597f454e, simplified imports;
2009-10-29 wenzelm 2009-10-29 merged
2009-10-29 haftmann 2009-10-29 merged
2009-10-29 haftmann 2009-10-29 adjusted to changes in theory Divides
2009-10-29 haftmann 2009-10-29 moved some lemmas to theory Int
2009-10-29 haftmann 2009-10-29 moved some dvd [int] facts to Int
2009-10-29 haftmann 2009-10-29 moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
2009-10-29 wenzelm 2009-10-29 eliminated some old folds;
2009-10-29 wenzelm 2009-10-29 eliminated some old folds;
2009-10-29 wenzelm 2009-10-29 eliminated some old folds;
2009-10-29 wenzelm 2009-10-29 less aggressive tracing;
2009-10-29 wenzelm 2009-10-29 DEEPEN: less aggressive tracing, subject to trace_DEEPEN;
2009-10-29 wenzelm 2009-10-29 merged
2009-10-29 wenzelm 2009-10-29 merged
2009-10-29 bulwahn 2009-10-29 removing ancient predicate compiler files
2009-10-29 bulwahn 2009-10-29 merged
2009-10-29 bulwahn 2009-10-29 encapsulating records with datatype constructors and adding type annotations to make SML/NJ happy
2009-10-28 bulwahn 2009-10-28 improved mode parser; added mode annotations to examples
2009-10-28 bulwahn 2009-10-28 moved datatype mode and string functions to the auxillary structure