2005-10-21 ago haftmann abandoned rational number functions in favor of General/rat.ML
2005-10-21 ago haftmann introduced functions from Pure/General/rat.ML
2005-10-21 ago haftmann slight corrections
2005-10-21 ago haftmann substantially improved integration of website into distribution framework
2005-10-21 ago haftmann substantially improved integration of website into distribution framework
2005-10-21 ago haftmann substantially improved integration of website into distribution framework
2005-10-21 ago haftmann substantially improved integration of website into distribution framework
2005-10-21 ago haftmann towards an improved website/makedist integration
2005-10-21 ago haftmann towards an improved website/makedist integration
2005-10-21 ago haftmann added default distinfo.mak
2005-10-21 ago haftmann towards an improved website/makedist integration
2005-10-21 ago haftmann towards an improved website/makedist integration
2005-10-21 ago haftmann added rounding functions
2005-10-21 ago mengj Merged theory ResAtpOracle.thy into ResAtpMethods.thy
2005-10-19 ago wenzelm obsolete;
2005-10-19 ago wenzelm removed add_inductive_x;
2005-10-19 ago wenzelm removed obsolete add_datatype_x;
2005-10-19 ago wenzelm removed obsolete thy_syntax.ML;
2005-10-19 ago wenzelm removed obsolete old_symbol_source;
2005-10-19 ago wenzelm removed obsolete non-Isar theory format and old Isar theory headers;
2005-10-19 ago wenzelm removed old-style theory format;
2005-10-19 ago wenzelm avoid lagacy read function;
2005-10-19 ago wenzelm added thm(s) retrieval functions (from goals.ML);
2005-10-19 ago wenzelm removed obsolete old-locales;
2005-10-19 ago wenzelm removed obsolete axclass_tac, add_inst_subclass_x, add_inst_arity_x;
2005-10-19 ago wenzelm removed obsolete Thy/thy_parse.ML, Thy/thy_scan.ML, Thy/thy_syn.ML;
2005-10-19 ago wenzelm removed obsolete old-style syntax;
2005-10-19 ago wenzelm removed obsolete IOA/meta_theory/ioa_package.ML;
2005-10-19 ago wenzelm removed obsolete domain/interface.ML, IOA/meta_theory/ioa_package.ML;
2005-10-19 ago wenzelm removed obsolete domain/interface.ML;
2005-10-19 ago wenzelm removed obsolete add_typedef_x;
2005-10-19 ago wenzelm removed print_exn (better let the toplevel do this);
2005-10-19 ago wenzelm removed obsolete add_recdef_old;
2005-10-19 ago wenzelm removed obsolete HOL/thy_syntax.ML;
2005-10-19 ago wenzelm * Theory syntax: discontinued non-Isar format and old Isar headers;
2005-10-19 ago wenzelm replaced commafy by existing commas;
2005-10-19 ago wenzelm updated;
2005-10-19 ago wenzelm isatool fixheaders;
2005-10-19 ago wenzelm fix headers;
2005-10-19 ago haftmann added table functor instance for pairs of strings
2005-10-19 ago haftmann added subgraph
2005-10-19 ago haftmann added join
2005-10-19 ago haftmann slight improvements for website
2005-10-19 ago wenzelm moved VAMPIRE_HOME, E_HOME to section "External reasoning tools" -- commented out by default!
2005-10-19 ago mengj More functions are added to the signature of ResClause
2005-10-19 ago mengj *** empty log message ***
2005-10-19 ago nipkow added 2 lemmas
2005-10-19 ago 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 ago wenzelm simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
2005-10-18 ago wenzelm tuned error msg;
2005-10-18 ago wenzelm renamed atomize_rule to atomize_cterm;
2005-10-18 ago wenzelm ObjectLogic.atomize_cterm;
2005-10-18 ago wenzelm use simplified Toplevel.proof etc.;
2005-10-18 ago wenzelm back: Toplevel.actual/skip_proof;
2005-10-18 ago wenzelm renamed set_context to context;
2005-10-18 ago wenzelm renamed set_context to context;
2005-10-18 ago wenzelm functor: no Simplifier argument;
2005-10-18 ago wenzelm moved helper lemma to HilbertChoice.thy;
2005-10-18 ago wenzelm Simplifier.theory_context;
2005-10-18 ago wenzelm added lemma exE_some (from specification_package.ML);