2005-10-19 wenzelm 2005-10-19 moved VAMPIRE_HOME, E_HOME to section "External reasoning tools" -- commented out by default!
2005-10-19 mengj 2005-10-19 More functions are added to the signature of ResClause
2005-10-19 mengj 2005-10-19 *** empty log message ***
2005-10-19 nipkow 2005-10-19 added 2 lemmas
2005-10-19 mengj 2005-10-19 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
2005-10-18 wenzelm 2005-10-18 simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
2005-10-18 wenzelm 2005-10-18 tuned error msg;
2005-10-18 wenzelm 2005-10-18 renamed atomize_rule to atomize_cterm;
2005-10-18 wenzelm 2005-10-18 ObjectLogic.atomize_cterm;
2005-10-18 wenzelm 2005-10-18 use simplified Toplevel.proof etc.;
2005-10-18 wenzelm 2005-10-18 back: Toplevel.actual/skip_proof; use simplified Toplevel.proof etc.;
2005-10-18 wenzelm 2005-10-18 renamed set_context to context; data extend: reset context;
2005-10-18 wenzelm 2005-10-18 renamed set_context to context; export theory_context; clear_ss: inherit_context; rewrite_aux etc.: theory_context;
2005-10-18 wenzelm 2005-10-18 functor: no Simplifier argument; Simplifier.theory_context;
2005-10-18 wenzelm 2005-10-18 moved helper lemma to HilbertChoice.thy; use actual ObjectLogic.atomize_cterm; eliminated obsolete sign_of;
2005-10-18 wenzelm 2005-10-18 Simplifier.theory_context; replaced get_const by Sign.the_const_type; eliminated obsolete sign_of;
2005-10-18 wenzelm 2005-10-18 added lemma exE_some (from specification_package.ML);
2005-10-18 wenzelm 2005-10-18 Simplifier.theory_context;
2005-10-18 wenzelm 2005-10-18 tuned error msg; tuned;
2005-10-18 wenzelm 2005-10-18 Simplifier.context/theory_context;
2005-10-18 wenzelm 2005-10-18 updated;
2005-10-18 paulson 2005-10-18 new interface to make_conjecture_clauses
2005-10-17 wenzelm 2005-10-17 * Simplifier: simpset of a running simplification process contains a proof context; * Simplifier.inherit_context supercedes Simplifier.inherit_bounds; * Simplifier/Classical Reasoner: more abstract interfaces change_simpset/claset;
2005-10-17 wenzelm 2005-10-17 added type_solver (uses Simplifier.the_context); removed obsolete context_type_solver;
2005-10-17 wenzelm 2005-10-17 added pos/negDivAlg_induct declarations (from Main.thy);
2005-10-17 wenzelm 2005-10-17 moved pos/negDivAlg_induct declarations to Integ/IntDiv.thy; change_simpset;
2005-10-17 wenzelm 2005-10-17 removed obsolete/experimental context components (superceded by Simplifier.the_context); more abstract change_simpset(_of); tuned;
2005-10-17 wenzelm 2005-10-17 added set/addloop' for simpset dependent loopers; simpset: added context field with the_context, set_context; added inherit_context (inherits bounds as well); removed obsolete inherit_bounds;
2005-10-17 wenzelm 2005-10-17 functor: no Simplifier argument; change_simpset;
2005-10-17 wenzelm 2005-10-17 change_claset(_of): more abtract interface; claset_of: init proof context; added raw get_claset;
2005-10-17 wenzelm 2005-10-17 functor: no Simplifier argument; export change_clasimpset;
2005-10-17 wenzelm 2005-10-17 tuned;
2005-10-17 wenzelm 2005-10-17 Simplifier.inherit_context instead of Simplifier.inherit_bounds;
2005-10-17 wenzelm 2005-10-17 change_claset/simpset;
2005-10-17 wenzelm 2005-10-17 change_claset/simpset; Simplifier.inherit_context instead of Simplifier.inherit_bounds;
2005-10-17 berghofe 2005-10-17 Improved proof of injectivity theorems to make it work on "ordinary" function types as well.
2005-10-17 berghofe 2005-10-17 Fixed bug in proof of support theorem (it failed on constructors with no arguments).
2005-10-17 berghofe 2005-10-17 Implemented proofs for support and freshness theorems.
2005-10-17 urbanc 2005-10-17 deleted leading space in the definition of fresh
2005-10-17 berghofe 2005-10-17 Initial revision.
2005-10-15 wenzelm 2005-10-15 tuned;
2005-10-15 wenzelm 2005-10-15 tuned comment;
2005-10-15 wenzelm 2005-10-15 added ML_type, ML_struct;
2005-10-15 wenzelm 2005-10-15 more;
2005-10-15 wenzelm 2005-10-15 * antiquotations ML_type, ML_struct; * Isar 'guess' element;
2005-10-15 wenzelm 2005-10-15 added guess;
2005-10-15 wenzelm 2005-10-15 added antiquotations ML_type, ML_struct;
2005-10-15 wenzelm 2005-10-15 use perl for test/stat;
2005-10-15 wenzelm 2005-10-15 export strip_params;
2005-10-15 wenzelm 2005-10-15 note_thmss, read/cert_vars etc.: natural argument order; added string_of_thm; tuned;
2005-10-15 wenzelm 2005-10-15 goal statements: before_qed argument;
2005-10-15 wenzelm 2005-10-15 added 'guess', which derives the obtained context from the course of reasoning;
2005-10-15 wenzelm 2005-10-15 added primitive_text, succeed_text;
2005-10-15 wenzelm 2005-10-15 goal statements: accomodate before_qed argument; ProofContext.note_thmss_i: natural argument order;
2005-10-15 wenzelm 2005-10-15 goal statements: accomodate before_qed argument;
2005-10-15 wenzelm 2005-10-15 added 'guess';
2005-10-15 wenzelm 2005-10-15 tuned;
2005-10-15 wenzelm 2005-10-15 added no_facts;
2005-10-15 wenzelm 2005-10-15 tuned comments;
2005-10-15 wenzelm 2005-10-15 updated;