2005-10-28 mengj 2005-10-28 Added "writeln_strs" to the signature
2005-10-28 mengj 2005-10-28 Added several new functions that are used to prove HOL goals. Added new methods "vampireH" and "eproverH" that can prove both FOL and HOL goals. The old "vampire" and "eprover" methods are renamed to "vampireF" and "eproverF"; they can only prove FOL goals.
2005-10-28 mengj 2005-10-28 Added new functions to handle HOL goals and lemmas. Added a funtion to send types and sorts information to ATP: they are clauses written to a separate file. Removed several functions definitions, and combined them with those in other files.
2005-10-28 mengj 2005-10-28 Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names. Also added function "repeat_RS" to the signature.
2005-10-28 mengj 2005-10-28 Added several functions to the signature. Added two new functions, which are used by res_hol_clause.ML programs.
2005-10-28 mengj 2005-10-28 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
2005-10-27 paulson 2005-10-27 sorted lemma lists
2005-10-27 wenzelm 2005-10-27 * HOL: alternative iff syntax;
2005-10-27 wenzelm 2005-10-27 consts: monomorphic;
2005-10-27 wenzelm 2005-10-27 removed inappropriate monomorphic test;
2005-10-27 wenzelm 2005-10-27 replaced Defs.monomorphic by Sign.monomorphic;
2005-10-27 wenzelm 2005-10-27 alternative iff syntax for equality on booleans, with print_mode 'iff';
2005-10-27 haftmann 2005-10-27 added module Pure/General/rat.ML
2005-10-26 paulson 2005-10-26 tidied away duplicate thm
2005-10-25 wenzelm 2005-10-25 EVERY;
2005-10-25 wenzelm 2005-10-25 traceIt: plain term;
2005-10-25 wenzelm 2005-10-25 val legacy = ref false;
2005-10-25 wenzelm 2005-10-25 prove_raw: cterms, explicit asms; prove: Pattern.matches beta_norm;
2005-10-25 wenzelm 2005-10-25 avoid legacy goals;
2005-10-22 wenzelm 2005-10-22 legacy = ref true for the time being -- avoid volumious warnings;
2005-10-21 wenzelm 2005-10-21 tuned;
2005-10-21 wenzelm 2005-10-21 avoid OldGoals shortcuts;
2005-10-21 wenzelm 2005-10-21 * Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running. * Internal goals: structure Goal.
2005-10-21 wenzelm 2005-10-21 Internal goals.
2005-10-21 wenzelm 2005-10-21 renamed triv_goal to goalI, rev_triv_goal to goalD;
2005-10-21 wenzelm 2005-10-21 tuned header;
2005-10-21 wenzelm 2005-10-21 Goal.norm_hhf_rule;
2005-10-21 wenzelm 2005-10-21 export add_binds_i; invoke_case: AutoBind.no_facts; Goal.init, Goal.conclude;
2005-10-21 wenzelm 2005-10-21 load_file: setmp OldGoals.legacy true;
2005-10-21 wenzelm 2005-10-21 improved check_result; Goal.init, Goal.conclude;
2005-10-21 wenzelm 2005-10-21 Goal.prove_plain;
2005-10-21 wenzelm 2005-10-21 do not export find_thms;
2005-10-21 wenzelm 2005-10-21 use obsolete goals.ML here;
2005-10-21 wenzelm 2005-10-21 Goal.conclude;
2005-10-21 wenzelm 2005-10-21 moved SELECT_GOAL to goal.ML;
2005-10-21 wenzelm 2005-10-21 moved norm_hhf_rule, prove etc. to goal.ML; moved asm_rewrite_goal_tac to simplifier.ML;
2005-10-21 wenzelm 2005-10-21 added simplification tactics and rules (from meta_simplifier.ML);
2005-10-21 wenzelm 2005-10-21 moved various simplification tactics and rules to simplifier.ML;
2005-10-21 wenzelm 2005-10-21 warn_obsolete for goal commands -- danger of disrupting a local proof context; Goal.init, Goal.conclude, Goal.norm_hhf_rule; shortcuts no longer pervasive (cf. structure OldGoals);
2005-10-21 wenzelm 2005-10-21 renamed triv_goal to goalI, rev_triv_goal to goalD; removed mk_triv_goal (cf. Goal.init);
2005-10-21 wenzelm 2005-10-21 added goal.ML; moved use of goals.ML;
2005-10-21 wenzelm 2005-10-21 added goal.ML;
2005-10-21 wenzelm 2005-10-21 Goal.norm_hhf_rule, Goal.init;
2005-10-21 wenzelm 2005-10-21 avoid triv_goal and home-grown meta_allE;
2005-10-21 wenzelm 2005-10-21 OldGoals;
2005-10-21 wenzelm 2005-10-21 proper header; proper use of ML files;
2005-10-21 wenzelm 2005-10-21 avoid home-grown meta_allE;
2005-10-21 wenzelm 2005-10-21 Goal.prove;
2005-10-21 wenzelm 2005-10-21 avoid shortcuts from OldGoals;
2005-10-21 wenzelm 2005-10-21 added simplified settings for Poly/ML 4.x (commented out);
2005-10-21 wenzelm 2005-10-21 reverted (accidental?) change of 1.148;
2005-10-21 haftmann 2005-10-21 abandoned rational number functions in favor of General/rat.ML
2005-10-21 haftmann 2005-10-21 introduced functions from Pure/General/rat.ML
2005-10-21 haftmann 2005-10-21 slight corrections
2005-10-21 haftmann 2005-10-21 substantially improved integration of website into distribution framework
2005-10-21 haftmann 2005-10-21 substantially improved integration of website into distribution framework
2005-10-21 haftmann 2005-10-21 substantially improved integration of website into distribution framework
2005-10-21 haftmann 2005-10-21 substantially improved integration of website into distribution framework
2005-10-21 haftmann 2005-10-21 towards an improved website/makedist integration
2005-10-21 haftmann 2005-10-21 towards an improved website/makedist integration