2005-10-29 urbanc 2005-10-29 1) have adjusted the swapping of the result type in add_datatype_i 2) have replaced map_nth_elem by Library.nth_map (there seems to be a clash with an existing nth_map somewhere - therefore the "Library")
2005-10-28 wenzelm 2005-10-28 tuned;
2005-10-28 wenzelm 2005-10-28 lthms_containing: not o valid_thms;
2005-10-28 wenzelm 2005-10-28 added fact_tac, some_fact_tac; retrieve_thms: support literal facts; tuned export interfaces;
2005-10-28 wenzelm 2005-10-28 renamed Goal constant to prop, more general protect/unprotect interfaces; tuned ProofContext.export interfaces;
2005-10-28 wenzelm 2005-10-28 renamed Goal constant to prop, more general protect/unprotect interfaces;
2005-10-28 wenzelm 2005-10-28 added fact method; accomodate simplified Thm.lift_rule;
2005-10-28 wenzelm 2005-10-28 tuned ProofContext.export interfaces;
2005-10-28 wenzelm 2005-10-28 syntax for literal facts;
2005-10-28 wenzelm 2005-10-28 removed try_dest_Goal, use Logic.unprotect;
2005-10-28 wenzelm 2005-10-28 added cgoal_of; simplified lift_rule: take goal cterm instead of goal state thm, use Logic.lift_abs/all;
2005-10-28 wenzelm 2005-10-28 accomodate simplified Thm.lift_rule; tuned;
2005-10-28 wenzelm 2005-10-28 export cong_modifiers, simp_modifiers';
2005-10-28 wenzelm 2005-10-28 certify_term: tuned monomorphic consts;
2005-10-28 wenzelm 2005-10-28 datatype thmref: added Fact; renamed Goal constant to prop;
2005-10-28 wenzelm 2005-10-28 Logic.lift_all;
2005-10-28 wenzelm 2005-10-28 renamed Goal constant to prop, more general protect/unprotect interfaces; replaced lift_fns by lift_abs, lift_all;
2005-10-28 wenzelm 2005-10-28 renamed Goal.norm_hhf_rule to Goal.norm_hhf;
2005-10-28 wenzelm 2005-10-28 renamed Goal constant to prop, more general protect/unprotect interfaces; renamed norm_hhf_rule to norm_hhf; added comp_hhf, compose_hhf_tac, based on Drule.lift_all;
2005-10-28 wenzelm 2005-10-28 added add_local/add_global; index props (for add_local only); added could_unify;
2005-10-28 wenzelm 2005-10-28 added incr_indexes; added lift_all (approx. reverse of gen_all); renamed Goal constant to prop, more general protect/unprotect interfaces;
2005-10-28 wenzelm 2005-10-28 renamed Goal constant to prop;
2005-10-28 wenzelm 2005-10-28 accomodate simplified Thm.lift_rule;
2005-10-28 wenzelm 2005-10-28 Logic.unprotect;
2005-10-28 wenzelm 2005-10-28 literal facts;
2005-10-28 wenzelm 2005-10-28 * Pure/Isar: literal facts; * ML/Pure: tuned Thm.lift_rule; * ML/Pure: renamed Goal constant to prop, more general uses;
2005-10-28 wenzelm 2005-10-28 tuned;
2005-10-28 webertj 2005-10-28 unnecessary imports removed
2005-10-28 urbanc 2005-10-28 fixed case names in the weak induction principle and changed name from "induct" to "induct_weak"
2005-10-28 berghofe 2005-10-28 Implemented proof of weak induction theorem.
2005-10-28 berghofe 2005-10-28 Added "deepen" method.
2005-10-28 haftmann 2005-10-28 circumvented smlnj value restriction
2005-10-28 haftmann 2005-10-28 added extraction interface for code generator
2005-10-28 urbanc 2005-10-28 Added (optional) arguments to the tactics perm_eq_simp and supports_simp. They now follow the "simp"-way and use the syntax: apply(supports_simp simp add: thms) etc.
2005-10-28 haftmann 2005-10-28 cleaned up nth, nth_update, nth_map and nth_string functions
2005-10-28 berghofe 2005-10-28 Removed legacy prove_goalw_cterm command.
2005-10-28 paulson 2005-10-28 got rid of obsolete prove_goalw_cterm
2005-10-28 haftmann 2005-10-28 swapped add_datatype result
2005-10-28 haftmann 2005-10-28 removed obfuscating PStrStrTab
2005-10-28 haftmann 2005-10-28 reachable - abandoned foldl_map in favor of fold_map
2005-10-28 mengj 2005-10-28 Added Tools/res_hol_clause.ML
2005-10-28 mengj 2005-10-28 Added a new file res_hol_clause.ML to Reconstruction.thy. This file is used to translate HOL formulae into FOL clauses.
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;