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;
2005-06-17 wenzelm 2005-06-17 Table.fold;
2005-06-17 wenzelm 2005-06-17 Symtab.fold;
2005-06-17 wenzelm 2005-06-17 type theory, theory_ref, exception THEORY and related operations imported from Context; actual theory content declared as theory data; removed syn_of; import theory operations in SIGN_THEORY from Sign; tuned;
2005-06-17 wenzelm 2005-06-17 obsolete type sg is now an alias for Context.theory; code and interfaces related to stamps and data now in context.ML; actual signature content declared as theory data; removed type sg_ref (superceded by theory_ref); signature SIGN_THEORY lists theory operations that are duplicated in Theory;
2005-06-17 wenzelm 2005-06-17 added theorem_space; removed unused extern_thm_sg; accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory; removed theory management (cf. 'history' in context.ML); moved add_typedecls to sign.ML; Sign.init, Theory.init; tuned;
2005-06-17 wenzelm 2005-06-17 Context.theory_name; tuned;
2005-06-17 wenzelm 2005-06-17 added serial numbers;
2005-06-17 wenzelm 2005-06-17 removed obsolete pretty printers for Theory.theory, Sign.sg; added pretty printer for Context.theory (long form of output);
2005-06-17 wenzelm 2005-06-17 removed pretty_theory, pprint_theory (see context.ML or thy_info.ML); removed obsolete pretty_name_space; accomodate identification of type Sign.sg and theory;
2005-06-17 wenzelm 2005-06-17 added type theory: generic theory contexts with unique identity, arbitrarily typed data, linear and graph development -- a complete rewrite of code that used to be spread over in sign.ML, theory.ML, theory_data.ML, pure_thy.ML;
2005-06-17 wenzelm 2005-06-17 removed Pure/theory_data.ML;
2005-06-17 wenzelm 2005-06-17 added Id;
2005-06-17 wenzelm 2005-06-17 Theory.merge;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory; Context.theory_name;
2005-06-17 wenzelm 2005-06-17 Context.theory_name;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory; Sign.the_const_type; Context.exists_name;