1999-09-26 ago wenzelm help: unknown theory context;
1999-09-26 ago wenzelm added keep', theory';
1999-09-26 ago wenzelm help: unkown theory context;
1999-09-26 ago wenzelm ThmDatabase.print_thms_containing;
1999-09-26 ago wenzelm added print_thms_containing;
1999-09-25 ago wenzelm defs: axmdecl;
1999-09-25 ago wenzelm simplified sectioned_args;
1999-09-25 ago wenzelm added reset_thms;
1999-09-25 ago wenzelm added reset_thms;
1999-09-25 ago wenzelm tuned;
1999-09-25 ago wenzelm defs: name mandatory;
1999-09-25 ago wenzelm avoid interrupts of read loop;
1999-09-25 ago wenzelm simplified sectioned_args;
1999-09-25 ago wenzelm Proof.reset_thms calculationN;
1999-09-25 ago wenzelm admit unbinding;
1999-09-25 ago wenzelm unfold / fold defs;
1999-09-25 ago wenzelm skolem_tag;
1999-09-25 ago wenzelm added fold_rule;
1999-09-24 ago wenzelm * HOL/Real/HahnBanach: the Hahn-Banach theorem for real vector spaces
1999-09-24 ago paulson working version with co-guarantees-leadsto results
1999-09-24 ago wenzelm tuned;
1999-09-24 ago wenzelm tuned;
1999-09-24 ago wenzelm qed "";
1999-09-23 ago wenzelm tuned print_result;
1999-09-23 ago wenzelm improved cycle error;
1999-09-23 ago paulson Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
1999-09-23 ago nipkow sep1 -> sep
1999-09-23 ago paulson The restrict_to_left rule fixes some bugs
1999-09-23 ago paulson Sets new component "restrict_to_left"
1999-09-23 ago paulson tidied; added lemma restrict_to_left
1999-09-23 ago nipkow Restructured lin.arith.package and fixed a proof in RComplete.
1999-09-23 ago nipkow Restructured lin.arith.package.
1999-09-22 ago wenzelm thms_containing: single writeln;
1999-09-22 ago wenzelm tuned pretty_thms;
1999-09-22 ago wenzelm added thms_containing;
1999-09-22 ago wenzelm qed "";
1999-09-22 ago wenzelm proper theory setup for Real/ex/BinEx;
1999-09-22 ago wenzelm tuned;
1999-09-22 ago wenzelm improved output;
1999-09-22 ago wenzelm added 'insert' method (again);
1999-09-22 ago wenzelm ml_store_thm: no warning for "";
1999-09-22 ago wenzelm present results;
1999-09-21 ago wenzelm merged in lost update;
1999-09-21 ago nipkow Mod because of new solver interface.
1999-09-21 ago nipkow ?
1999-09-21 ago nipkow Solvers are now named and stamped.
1999-09-21 ago wenzelm fixed unfold of facts;
1999-09-21 ago wenzelm accomodate refined facts handling;
1999-09-21 ago wenzelm accomodate refined facts handling;
1999-09-21 ago wenzelm Main;
1999-09-21 ago wenzelm Thm.no_prems;
1999-09-21 ago wenzelm tuned;
1999-09-21 ago wenzelm added some ~= rules;
1999-09-21 ago wenzelm removed "case" thm;
1999-09-21 ago wenzelm setup for refined facts handling;
1999-09-21 ago wenzelm setup for refined facts handling;
1999-09-21 ago wenzelm export prems_of;
1999-09-21 ago wenzelm setup_goal: do not insert assumptions;
1999-09-21 ago wenzelm setup for refined facts handling;
1999-09-21 ago wenzelm differ: compare actual props only (hyps may changed due to trivial steps involving assumptions);