2005-10-19 mengj *** empty log message ***
2005-10-19 nipkow added 2 lemmas
2005-10-19 mengj 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 simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
2005-10-18 wenzelm tuned error msg;
2005-10-18 wenzelm renamed atomize_rule to atomize_cterm;
2005-10-18 wenzelm ObjectLogic.atomize_cterm;
2005-10-18 wenzelm use simplified Toplevel.proof etc.;
2005-10-18 wenzelm back: Toplevel.actual/skip_proof;
2005-10-18 wenzelm renamed set_context to context;
2005-10-18 wenzelm renamed set_context to context;
2005-10-18 wenzelm functor: no Simplifier argument;
2005-10-18 wenzelm moved helper lemma to HilbertChoice.thy;
2005-10-18 wenzelm Simplifier.theory_context;
2005-10-18 wenzelm added lemma exE_some (from specification_package.ML);
2005-10-18 wenzelm Simplifier.theory_context;
2005-10-18 wenzelm tuned error msg;
2005-10-18 wenzelm Simplifier.context/theory_context;
2005-10-18 wenzelm updated;
2005-10-18 paulson new interface to make_conjecture_clauses
2005-10-17 wenzelm * Simplifier: simpset of a running simplification process contains a proof context;
2005-10-17 wenzelm added type_solver (uses Simplifier.the_context);
2005-10-17 wenzelm added pos/negDivAlg_induct declarations (from Main.thy);
2005-10-17 wenzelm moved pos/negDivAlg_induct declarations to Integ/IntDiv.thy;
2005-10-17 wenzelm removed obsolete/experimental context components (superceded by Simplifier.the_context);
2005-10-17 wenzelm added set/addloop' for simpset dependent loopers;
2005-10-17 wenzelm functor: no Simplifier argument;
2005-10-17 wenzelm change_claset(_of): more abtract interface;
2005-10-17 wenzelm functor: no Simplifier argument;
2005-10-17 wenzelm tuned;
2005-10-17 wenzelm Simplifier.inherit_context instead of Simplifier.inherit_bounds;
2005-10-17 wenzelm change_claset/simpset;
2005-10-17 wenzelm change_claset/simpset;
2005-10-17 berghofe Improved proof of injectivity theorems to make it work on
2005-10-17 berghofe Fixed bug in proof of support theorem (it failed on constructors with no arguments).
2005-10-17 berghofe Implemented proofs for support and freshness theorems.
2005-10-17 urbanc deleted leading space in the definition of fresh
2005-10-17 berghofe Initial revision.
2005-10-14 wenzelm tuned;
2005-10-14 wenzelm tuned comment;
2005-10-14 wenzelm added ML_type, ML_struct;
2005-10-14 wenzelm more;
2005-10-14 wenzelm * antiquotations ML_type, ML_struct;
2005-10-14 wenzelm added guess;
2005-10-14 wenzelm added antiquotations ML_type, ML_struct;
2005-10-14 wenzelm use perl for test/stat;
2005-10-14 wenzelm export strip_params;
2005-10-14 wenzelm note_thmss, read/cert_vars etc.: natural argument order;
2005-10-14 wenzelm goal statements: before_qed argument;
2005-10-14 wenzelm added 'guess', which derives the obtained context from the course of reasoning;
2005-10-14 wenzelm added primitive_text, succeed_text;
2005-10-14 wenzelm goal statements: accomodate before_qed argument;
2005-10-14 wenzelm goal statements: accomodate before_qed argument;
2005-10-14 wenzelm added 'guess';
2005-10-14 wenzelm tuned;
2005-10-14 wenzelm added no_facts;
2005-10-14 wenzelm tuned comments;
2005-10-14 wenzelm updated;
2005-10-14 paulson signature changes
2005-10-14 haftmann added module rat.ML for rational numbers
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip