2009-11-02 huffman 2009-11-02 add fixrec support for HOL pair constructor patterns
2009-11-02 huffman 2009-11-02 define cprod_fun using Pair instead of cpair
2009-11-02 huffman 2009-11-02 add (LAM (x, y). t) syntax and lemma csplit_Pair
2009-11-02 krauss 2009-11-02 lexicographic order: run local descent proofs in parallel
2009-11-02 huffman 2009-11-02 merged
2009-11-02 huffman 2009-11-02 domain package no longer uses cfst/csnd/cpair
2009-11-02 krauss 2009-11-02 conceal partial rules depending on config flag (i.e. when called via "fun")
2009-11-02 krauss 2009-11-02 conceal "termination" rule, used only by special tools
2009-11-02 krauss 2009-11-02 do not use Binding.empty: conceal flag gets lost in Thm.def_binding_optional
2009-11-02 wenzelm 2009-11-02 modernized structure XML_Syntax;
2009-11-02 wenzelm 2009-11-02 structure Thm_Deps;
2009-11-02 wenzelm 2009-11-02 modernized structure Proof_Node;
2009-11-02 wenzelm 2009-11-02 modernized structure Proof_Display;
2009-11-02 wenzelm 2009-11-02 modernized structure Proof_Syntax;
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