2005-06-21 nipkow 2005-06-21 added find thms section
2005-06-21 wenzelm 2005-06-21 proper implementation of pointer_eq;
2005-06-21 wenzelm 2005-06-21 tuned pointer_eq;
2005-06-21 paulson 2005-06-21 VAMPIRE_HOME, helper_path and various stylistic tweaks
2005-06-21 kleing 2005-06-21 lemma, equation between rtrancl and trancl
2005-06-21 wenzelm 2005-06-21 enter_thms: use theorem database of thy *after* attribute application;
2005-06-21 wenzelm 2005-06-21 tuned;
2005-06-21 wenzelm 2005-06-21 added subset, eq_set; tuned insert/remove: avoid garbage;
2005-06-21 wenzelm 2005-06-21 tuned SUBGOAL: Logic.nth_prem instead of List.nth o prems_of;
2005-06-21 wenzelm 2005-06-21 fixed HOL-Complex-Matrix target;
2005-06-21 haftmann 2005-06-21 removed mkcontent from makedist
2005-06-21 kleing 2005-06-21 fix 'give up waiting message' (logs of running processes are not attached)
2005-06-20 wenzelm 2005-06-20 * Pure: get_thm interface expects datatype thmref; * More efficient treatment of intermediate theory checkpoints;
2005-06-20 wenzelm 2005-06-20 avoid identifier 'Name';
2005-06-20 wenzelm 2005-06-20 Theory.begin/end_theory;
2005-06-20 wenzelm 2005-06-20 clarify empty vs. pure browser info;
2005-06-20 wenzelm 2005-06-20 added pointer_eq;
2005-06-20 wenzelm 2005-06-20 thmref: Name vs. NameSelection; tuned;
2005-06-20 wenzelm 2005-06-20 refl_tac: avoid failure of unification, i.e. confusing trace msg; get_thm(s): Name;
2005-06-20 wenzelm 2005-06-20 print_theorems: proper use of PureThy.print_theorems_diff;
2005-06-20 wenzelm 2005-06-20 thmref: Name vs. NameSelection;
2005-06-20 wenzelm 2005-06-20 generalized type of inter; added substract; economize heap usage;
2005-06-20 wenzelm 2005-06-20 added previous;
2005-06-20 wenzelm 2005-06-20 added begin_theory, end_theory;
2005-06-20 wenzelm 2005-06-20 added certify_prop, cert_term, cert_prop;
2005-06-20 wenzelm 2005-06-20 datatype thmref = Name ... | NameSelection ...; added print_theorems_diff; tuned;
2005-06-20 wenzelm 2005-06-20 added member, option_ord;
2005-06-20 wenzelm 2005-06-20 OrdList.inter;
2005-06-20 wenzelm 2005-06-20 tuned;
2005-06-20 wenzelm 2005-06-20 improved treatment of intermediate checkpoints: actual copy instead of extend, purge after end; tuned;
2005-06-20 wenzelm 2005-06-20 added add_fixrec_i, add_fixpat_i; ThyParse obsolete; Sign.read_prop, Sign.cert_prop;
2005-06-20 wenzelm 2005-06-20 proper header;
2005-06-20 wenzelm 2005-06-20 get_thm(s): Name;
2005-06-20 wenzelm 2005-06-20 get_thm instead of obsolete Goals.get_thm; improved msg;
2005-06-20 wenzelm 2005-06-20 HOL-Matrix: plain session;
2005-06-20 wenzelm 2005-06-20 removed obsolete print_depth;
2005-06-20 wenzelm 2005-06-20 be less ambitious about the author's name; tuned generated root.tex;
2005-06-20 wenzelm 2005-06-20 exclude pghead.pdf from doc;
2005-06-20 wenzelm 2005-06-20 improved formatting;
2005-06-20 wenzelm 2005-06-20 use Tools/ATP/VampCommunication.ML;
2005-06-20 quigley 2005-06-20 Added VampCommunication.ML. Changed small set of Spass rules to Ordered version. Fixed printing out of resolution proofs if parsing/translation fails.
2005-06-20 wenzelm 2005-06-20 moved configure to lib/scripts;
2005-06-20 wenzelm 2005-06-20 ./configure obsolete on virtually all systems, but apt to cause problems;
2005-06-20 paulson 2005-06-20 using TPTP2X_HOME; indentation, etc
2005-06-20 paulson 2005-06-20 fixed a faulty proof
2005-06-20 paulson 2005-06-20 moving some generic inequalities from integer arith to nat arith
2005-06-20 haftmann 2005-06-20 (moved to Distribution/lib/scripts)
2005-06-20 haftmann 2005-06-20 added fixheaders
2005-06-19 wenzelm 2005-06-19 improved comment;
2005-06-19 wenzelm 2005-06-19 some minor adaptions to make it work again;
2005-06-18 wenzelm 2005-06-18 tuned;
2005-06-18 wenzelm 2005-06-18 tuned remove;
2005-06-18 wenzelm 2005-06-18 added member;
2005-06-18 wenzelm 2005-06-18 added Pure/General/ord_list.ML;
2005-06-18 wenzelm 2005-06-18 Ordered lists without duplicates.
2005-06-18 huffman 2005-06-18 fixrec shows unsolved subgoals when proofs of rewrites fail
2005-06-18 huffman 2005-06-18 make match_rews into simp rules by default
2005-06-17 huffman 2005-06-17 support theorem names and attributes for fixrec equations; also make them into simp rules by default, like primrec does
2005-06-17 huffman 2005-06-17 added match functions for ONE, TT, and FF; added theorem mplus_fail2
2005-06-17 wenzelm 2005-06-17 updated;