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;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory;
2005-06-17 wenzelm 2005-06-17 Context.names_of;
2005-06-17 wenzelm 2005-06-17 * Pure/TheoryDataFun: change of the argument structure; * Pure/TheoryDataFun: change of the argument structure -- got rid of Sign.sg;
2005-06-17 wenzelm 2005-06-17 Sign.root_path, Sign.local_path;
2005-06-17 wenzelm 2005-06-17 removed obsolete theory_of_sign, theory_of_thm; Context.draftN; Context.begin_theory;
2005-06-17 wenzelm 2005-06-17 PolyML.Compiler.printInAlphabeticalOrder := false;
2005-06-17 wenzelm 2005-06-17 Context.DATA_FAIL; accomodate identification of type Sign.sg and theory;
2005-06-17 wenzelm 2005-06-17 Context.PureN;
2005-06-17 wenzelm 2005-06-17 RuleCases.tactic; accomodate identification of type Sign.sg and theory;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory; tuned;
2005-06-17 wenzelm 2005-06-17 (RAW_)METHOD_CASES: RuleCases.tactic; accomodate change of TheoryDataFun;
2005-06-17 wenzelm 2005-06-17 Theory.add_typedecls; Sign.local_path;
2005-06-17 wenzelm 2005-06-17 added map', fold; changed join to pass key;